Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 53394 f26f00cbd573
parent 53390 51b562922cb1
child 55587 5d3db2c626e3 
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Sep 03 21:46:41 2013 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Sep 03 21:46:41 2013 +0100
@@ -86,7 +86,7 @@
     | Term_Conditional of tptp_formula * tptp_term * tptp_term
     | Term_Num of number_kind * string
     | Term_Distinct_Object of string
-    | Term_Let of tptp_let list * tptp_term (*FIXME remove list?*)
+    | Term_Let of tptp_let * tptp_term
 
   and tptp_atom =
       TFF_Typed_Atom of symbol * tptp_type option (*only TFF*)
@@ -99,14 +99,14 @@
     | Sequent of tptp_formula list * tptp_formula list
     | Quant of quantifier * (string * tptp_type option) list * tptp_formula
     | Conditional of tptp_formula * tptp_formula * tptp_formula
-    | Let of tptp_let list * tptp_formula (*FIXME remove list?*)
+    | Let of tptp_let * tptp_formula
     | Atom of tptp_atom
     | Type_fmla of tptp_type
     | THF_typing of tptp_formula * tptp_type (*only THF*)
 
   and tptp_let =
-      Let_fmla of (string * tptp_type option) * tptp_formula
-    | Let_term of (string * tptp_type option) * tptp_term (*only TFF*)
+      Let_fmla of (string * tptp_type option) list * tptp_formula
+    | Let_term of (string * tptp_type option) list * tptp_term
 
   and tptp_type =
       Prod_type of tptp_type * tptp_type
@@ -234,7 +234,7 @@
     | Term_Conditional of tptp_formula * tptp_term * tptp_term
     | Term_Num of number_kind * string
     | Term_Distinct_Object of string
-    | Term_Let of tptp_let list * tptp_term (*FIXME remove list?*)
+    | Term_Let of tptp_let * tptp_term
 
   and tptp_atom =
       TFF_Typed_Atom of symbol * tptp_type option (*only TFF*)
@@ -247,14 +247,14 @@
     | Sequent of tptp_formula list * tptp_formula list
     | Quant of quantifier * (string * tptp_type option) list * tptp_formula
     | Conditional of tptp_formula * tptp_formula * tptp_formula
-    | Let of tptp_let list * tptp_formula
+    | Let of tptp_let * tptp_formula
     | Atom of tptp_atom
     | Type_fmla of tptp_type
     | THF_typing of tptp_formula * tptp_type
 
   and tptp_let =
-      Let_fmla of (string * tptp_type option) * tptp_formula
-    | Let_term of (string * tptp_type option) * tptp_term
+      Let_fmla of (string * tptp_type option) list * tptp_formula
+    | Let_term of (string * tptp_type option) list * tptp_term
 
   and tptp_type =
       Prod_type of tptp_type * tptp_type
isabelle