Commit e6e6070f authored by Francois Bobot's avatar Francois Bobot
Browse files

Correction des bads pour la nouvelle syntaxe

parent 7ce19416
theory A end theory A end
theory B uses A, A end theory B use A use A end
theory A end theory A end
theory B end theory B end
theory C uses A, A:B end theory C use A use B as A end
...@@ -3,5 +3,5 @@ theory A ...@@ -3,5 +3,5 @@ theory A
end end
theory B theory B
uses A use A
end end
...@@ -135,8 +135,7 @@ Keywords are the following: ...@@ -135,8 +135,7 @@ Keywords are the following:
%% file := decl* %% file := decl*
%% decl := | "theory" uident decl* "end" %% decl := | "theory" uident decl* "end"
%% | "theory" uident "." uqualid ("with" instance+ )? %% | "theory" uident "." uqualid ("with" instance+ )?
%% | "use" "open"? uqualid ("as" ident) %% | "use" ("open" | "include")? uqualid ("as" ident)
%% | "use" "include" uqualid %% pas de as pour include
%% | ("axiom"|"lemma"|"goal") ident ":" fmla %% | ("axiom"|"lemma"|"goal") ident ":" fmla
%% | "type" typarams lident ("=" (ty-alg | ty))? %% | "type" typarams lident ("=" (ty-alg | ty))?
%% ("and" typarams lident ("=" (ty-alg | ty))?)* %% ("and" typarams lident ("=" (ty-alg | ty))?)*
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment