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/Tools/ATP/recon_parse.ML
changeset 16357 f1275d2a1dee
parent 16061 8a139c1557bf
child 16418 5d0d24bd2c96 
--- a/src/HOL/Tools/ATP/recon_parse.ML	Thu Jun 09 23:33:28 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML	Fri Jun 10 16:15:36 2005 +0200
@@ -212,6 +212,21 @@
                    ++ term_num
             >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
       
+      val super_l  = (a (Word "SpL")) ++ (a (Other ":"))
+                   ++ term_num ++ (a (Other ","))
+                   ++ term_num
+            >> (fn (_, (_, (c, (_, e)))) => Super_l (c, e))
+
+
+      val super_r  = (a (Word "SpR")) ++ (a (Other ":"))
+                   ++ term_num ++ (a (Other ","))
+                   ++ term_num
+            >> (fn (_, (_, (c, (_, e)))) => Super_r (c, e))
+
+
+      val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num
+                 >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
+
       val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
                     ++ term_num ++ (a (Other ",")) 
                     ++ term_num
@@ -223,10 +238,27 @@
                    ++ term_num
             >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
 
+      val ssi = (a (Word "SSi")) ++ (a (Other ":"))
+                   ++ term_num ++ (a (Other ","))
+                   ++ term_num
+            >> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e))
+
+    val unc = (a (Word "UnC")) ++ (a (Other ":"))
+                   ++ term_num ++ (a (Other ","))
+                   ++ term_num
+            >> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e))
+
+
 
       val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
                  >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
-     
+
+      val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num
+                 >> (fn (_, (_, c)) => EqualRes ((fst c),(snd c)))
+   
+      val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num
+                 >> (fn (_, (_, c)) => Condense ((fst c),(snd c)))
+
 (*
       val hyper = a (Word "hyper")
                   ++ many ((a (Other ",") ++ number) >> snd)
@@ -234,7 +266,8 @@
 *)
      (* val method = axiom ||binary || factor || para || hyper*)
 
-      val method = axiom || binary || factor || para || rewrite || mrr || obv
+      val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con
+
       val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
             >> (fn (_, (_, a)) => Binary_s a)
       val factor_s = a (Word "factor_s")
@@ -316,7 +349,9 @@
         || word ++ a (Other "(") ++  arglist ++ a (Other ")") 
            >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
 
-        || word >> (fn w => "~"^" "^(remove_typeinfo w))) input
+        || word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w))
+
+        || word                  >> (fn w => "~"^" "^(remove_typeinfo w))) input
 
 and  nterm input =
     
@@ -338,7 +373,9 @@
         || word ++ a (Other "(") ++ arglist ++ a (Other ")") 
            >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
 
-        || word >> (fn w =>  (remove_typeinfo w)) ) input 
+        || word ++ a (Other "*") >> (fn (w,b) =>  (remove_typeinfo w)) 
+        || word                  >> (fn w =>  (remove_typeinfo w)) 
+         ) input 
 
 
 and peqterm input =(
isabelle