Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
val atomize = thms "atomize'";
authorwenzelm
Fri, 10 Nov 2000 19:00:22 +0100
changeset 10429 8820f787e61e
parent 10428 8f15fbce549f
child 10430 d3f780c3af0c
val atomize = thms "atomize'";
src/FOL/blastdata.ML file | annotate | diff | comparison | revisions
src/FOL/cladata.ML file | annotate | diff | comparison | revisions
src/HOL/blastdata.ML file | annotate | diff | comparison | revisions
src/HOL/cladata.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/blastdata.ML	Fri Nov 10 16:31:28 2000 +0100
+++ b/src/FOL/blastdata.ML	Fri Nov 10 19:00:22 2000 +0100
@@ -10,7 +10,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Cla.claset
   val rep_cs    = Cla.rep_cs
-  val atomize	= thms "atomize"
+  val atomize	= thms "atomize'"
   val cla_modifiers = Cla.cla_modifiers;
   val cla_meth' = Cla.cla_meth'
   end;
--- a/src/FOL/cladata.ML	Fri Nov 10 16:31:28 2000 +0100
+++ b/src/FOL/cladata.ML	Fri Nov 10 19:00:22 2000 +0100
@@ -24,7 +24,7 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= thms "atomize"
+  val atomize	= thms "atomize'"
   end;
 
 structure Cla = ClassicalFun(Classical_Data);
--- a/src/HOL/blastdata.ML	Fri Nov 10 16:31:28 2000 +0100
+++ b/src/HOL/blastdata.ML	Fri Nov 10 19:00:22 2000 +0100
@@ -23,7 +23,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Classical.claset
   val rep_cs    = Classical.rep_cs
-  val atomize	= thms "atomize"
+  val atomize	= thms "atomize'"
   val cla_modifiers = Classical.cla_modifiers;
   val cla_meth' = Classical.cla_meth'
   end;
--- a/src/HOL/cladata.ML	Fri Nov 10 16:31:28 2000 +0100
+++ b/src/HOL/cladata.ML	Fri Nov 10 19:00:22 2000 +0100
@@ -47,7 +47,7 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= thms "atomize"
+  val atomize	= thms "atomize'"
   end;
 
 structure Classical = ClassicalFun(Classical_Data);
isabelle