val atomize = thms "atomize'";
authorwenzelm
Fri Nov 10 19:00:22 2000 +0100 (2000-11-10)
changeset 104298820f787e61e
parent 10428 8f15fbce549f
child 10430 d3f780c3af0c
val atomize = thms "atomize'";
src/FOL/blastdata.ML
src/FOL/cladata.ML
src/HOL/blastdata.ML
src/HOL/cladata.ML
     1.1 --- a/src/FOL/blastdata.ML	Fri Nov 10 16:31:28 2000 +0100
     1.2 +++ b/src/FOL/blastdata.ML	Fri Nov 10 19:00:22 2000 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     1.5    val claset	= Cla.claset
     1.6    val rep_cs    = Cla.rep_cs
     1.7 -  val atomize	= thms "atomize"
     1.8 +  val atomize	= thms "atomize'"
     1.9    val cla_modifiers = Cla.cla_modifiers;
    1.10    val cla_meth' = Cla.cla_meth'
    1.11    end;
     2.1 --- a/src/FOL/cladata.ML	Fri Nov 10 16:31:28 2000 +0100
     2.2 +++ b/src/FOL/cladata.ML	Fri Nov 10 19:00:22 2000 +0100
     2.3 @@ -24,7 +24,7 @@
     2.4    val classical = classical
     2.5    val sizef     = size_of_thm
     2.6    val hyp_subst_tacs=[hyp_subst_tac]
     2.7 -  val atomize	= thms "atomize"
     2.8 +  val atomize	= thms "atomize'"
     2.9    end;
    2.10  
    2.11  structure Cla = ClassicalFun(Classical_Data);
     3.1 --- a/src/HOL/blastdata.ML	Fri Nov 10 16:31:28 2000 +0100
     3.2 +++ b/src/HOL/blastdata.ML	Fri Nov 10 19:00:22 2000 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     3.5    val claset	= Classical.claset
     3.6    val rep_cs    = Classical.rep_cs
     3.7 -  val atomize	= thms "atomize"
     3.8 +  val atomize	= thms "atomize'"
     3.9    val cla_modifiers = Classical.cla_modifiers;
    3.10    val cla_meth' = Classical.cla_meth'
    3.11    end;
     4.1 --- a/src/HOL/cladata.ML	Fri Nov 10 16:31:28 2000 +0100
     4.2 +++ b/src/HOL/cladata.ML	Fri Nov 10 19:00:22 2000 +0100
     4.3 @@ -47,7 +47,7 @@
     4.4    val classical = classical
     4.5    val sizef     = size_of_thm
     4.6    val hyp_subst_tacs=[hyp_subst_tac]
     4.7 -  val atomize	= thms "atomize"
     4.8 +  val atomize	= thms "atomize'"
     4.9    end;
    4.10  
    4.11  structure Classical = ClassicalFun(Classical_Data);