grammar org.xtext.example.mydsl1.MyDsl with org.eclipse.xtext.common.Terminals

generate myDsl "http://www.xtext.org/example/mydsl1/MyDsl"
      
    Primary returns Expression:
      ID;

grammar org.abos.mizar.mse.Common with org.eclipse.xtext.common.Terminals

import "http://www.eclipse.org/emf/2002/Ecore" as ecore

Theorem:
	'theorem' CompactStatement
;

CompactStatement:
	Proposition Justification ';'
;

Proposition:
	Sentence // TODO change
	// (LabelId ':')? Sentence
;

Sentence:
	FormulaExpr
;

Justification:
	SimpleJustification | Proof
;

SimpleJustification:
	SfwJustification
;

SfwJustification: // straightforward justification
	'by' References
;

Proof:
	'proof' Reasoning 'end'
;

//------------------------
// References
//------------------------

ArticleName:
	ID
;

LabelId:
	ID
;

References:
	Reference (',' Reference)*
;

Reference:
	LocalReference | LibraryReference
;

LocalReference:
	LabelId
;

LibraryReference:
	ArticleName ':' (INT | 'def' INT)
;

//------------------------
// Reasoning
//------------------------

Reasoning:
	ID // TODO change
;

//------------------------
// Formulas
//------------------------

FormulaExpr returns Expression:
	ID // TODO change
;