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/atp_problem.ML
changeset 54197 994ebb795b75
parent 53586 bd5fa6425993
child 54788 a898e15b522a 
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Oct 24 12:43:33 2013 +0200
@@ -33,14 +33,13 @@
 
   datatype polymorphism = Monomorphic | Polymorphic
   datatype thf_choice = THF_Without_Choice | THF_With_Choice
-  datatype thf_defs = THF_Without_Defs | THF_With_Defs
 
   datatype atp_format =
     CNF |
     CNF_UEQ |
     FOF |
     TFF of polymorphism |
-    THF of polymorphism * thf_choice * thf_defs |
+    THF of polymorphism * thf_choice |
     DFG of polymorphism
 
   datatype atp_formula_role =
@@ -179,14 +178,13 @@
 
 datatype polymorphism = Monomorphic | Polymorphic
 datatype thf_choice = THF_Without_Choice | THF_With_Choice
-datatype thf_defs = THF_Without_Defs | THF_With_Defs
 
 datatype atp_format =
   CNF |
   CNF_UEQ |
   FOF |
   TFF of polymorphism |
-  THF of polymorphism * thf_choice * thf_defs |
+  THF of polymorphism * thf_choice |
   DFG of polymorphism
 
 datatype atp_formula_role =
isabelle