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.yacc
changeset 57808 cf72aed038c8
parent 53395 a1a78a271682 
--- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Thu Aug 07 12:17:41 2014 +0200
@@ -491,7 +491,7 @@
 tff_unitary_type : tff_atomic_type               (( tff_atomic_type ))
                  | LPAREN tff_xprod_type RPAREN  (( tff_xprod_type ))
 
-tff_atomic_type : atomic_word   (( Atom_type atomic_word ))
+tff_atomic_type : atomic_word   (( Atom_type (atomic_word, []) ))
                 | defined_type  (( Defined_type defined_type ))
                 | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) ))
                 | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
@@ -634,6 +634,7 @@
   | "$real" => Type_Real
   | "$rat" => Type_Rat
   | "$int" => Type_Int
+  | "$_" => Type_Dummy
   | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
 ))
 
@@ -747,6 +748,7 @@
   | "$real" => TypeSymbol Type_Real
   | "$rat" => TypeSymbol Type_Rat
   | "$tType" => TypeSymbol Type_Type
+  | "$_" => TypeSymbol Type_Dummy
 
   | "$true" => Interpreted_Logic True
   | "$false" => Interpreted_Logic False
isabelle