# HG changeset patch
# User wenzelm
# Date 1003090507 -7200
# Node ID b7b100a2de1d0a8223a97633ee0b804ee27be419
# Parent  b6bb7a853dd26238368368f2ade7150fbd97232b
moved rulify to ObjectLogic;

diff -r b6bb7a853dd2 -r b7b100a2de1d TFL/post.ML
--- a/TFL/post.ML	Sun Oct 14 22:08:29 2001 +0200
+++ b/TFL/post.ML	Sun Oct 14 22:15:07 2001 +0200
@@ -171,8 +171,8 @@
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
-       val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules)
-   in  {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')),
+       val rules' = map (standard o ObjectLogic.rulify_no_asm) (R.CONJUNCTS rules)
+   in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
         rules = ListPair.zip(rules', rows),
         tcs = (termination_goals rules') @ tcs}
    end
diff -r b6bb7a853dd2 -r b7b100a2de1d src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sun Oct 14 22:08:29 2001 +0200
+++ b/src/FOL/FOL.thy	Sun Oct 14 22:15:07 2001 +0200
@@ -35,8 +35,6 @@
 setup "Simplifier.method_setup Splitter.split_modifiers"
 setup Splitter.setup
 setup Clasimp.setup
-setup Rulify.setup
-
 
 
 subsection {* Proof by cases and induction *}
diff -r b6bb7a853dd2 -r b7b100a2de1d src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Oct 14 22:08:29 2001 +0200
+++ b/src/FOL/IFOL.thy	Sun Oct 14 22:15:07 2001 +0200
@@ -158,4 +158,6 @@
   thus "x == y" by (rule eq_reflection)
 qed
 
+declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
+
 end
diff -r b6bb7a853dd2 -r b7b100a2de1d src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Sun Oct 14 22:08:29 2001 +0200
+++ b/src/FOL/IsaMakefile	Sun Oct 14 22:15:07 2001 +0200
@@ -29,7 +29,7 @@
 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	$(SRC)/Provers/make_elim.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
-  $(SRC)/Provers/rulify.ML $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
+  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
   FOL.ML FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \
   IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \
   fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
diff -r b6bb7a853dd2 -r b7b100a2de1d src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Sun Oct 14 22:08:29 2001 +0200
+++ b/src/FOL/ROOT.ML	Sun Oct 14 22:15:07 2001 +0200
@@ -14,7 +14,6 @@
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/ind.ML";
 use "~~/src/Provers/hypsubst.ML";
-use "~~/src/Provers/rulify.ML";
 use "~~/src/Provers/induct_method.ML";
 use "~~/src/Provers/make_elim.ML";
 use "~~/src/Provers/classical.ML";
diff -r b6bb7a853dd2 -r b7b100a2de1d src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sun Oct 14 22:08:29 2001 +0200
+++ b/src/FOL/simpdata.ML	Sun Oct 14 22:15:07 2001 +0200
@@ -364,20 +364,3 @@
 open Clasimp;
 
 val FOL_css = (FOL_cs, FOL_ss);
-
-
-(* rulify setup *)
-
-local
-  val ss = FOL_basic_ss addsimps
-    [Drule.norm_hhf_eq, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
-in
-
-structure Rulify = RulifyFun
- (val make_meta = Simplifier.simplify ss
-  val full_make_meta = Simplifier.full_simplify ss);
-
-structure BasicRulify: BASIC_RULIFY = Rulify;
-open BasicRulify;
-
-end;
diff -r b6bb7a853dd2 -r b7b100a2de1d src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Sun Oct 14 22:08:29 2001 +0200
+++ b/src/Provers/induct_method.ML	Sun Oct 14 22:15:07 2001 +0200
@@ -148,10 +148,10 @@
 
 fun atomize_cterm ct =
   Thm.cterm_fun
-    (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct))) (full_rewrite_cterm Data.atomize ct);
+    (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct))) (rewrite_cterm true Data.atomize ct);
 
 val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
-val rulify_cterm = full_rewrite_cterm Data.rulify2 o full_rewrite_cterm Data.rulify1;
+val rulify_cterm = rewrite_cterm true Data.rulify2 o rewrite_cterm true Data.rulify1;
 
 val rulify_tac =
   Tactic.rewrite_goal_tac Data.rulify1 THEN'
diff -r b6bb7a853dd2 -r b7b100a2de1d src/Provers/rulify.ML
--- a/src/Provers/rulify.ML	Sun Oct 14 22:08:29 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-(*  Title:      Provers/rulify.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-Conversion of object-level -->/ALL into meta-level ==>/!!.
-*)
-
-signature BASIC_RULIFY =
-sig
-  val rulify: thm -> thm
-  val rulify_no_asm: thm -> thm
-  val qed_spec_mp: string -> unit
-  val qed_goal_spec_mp: string -> theory -> string -> (thm list -> tactic list) -> unit
-  val qed_goalw_spec_mp: string -> theory -> thm list -> string
-    -> (thm list -> tactic list) -> unit
-end;
-
-signature RULIFY =
-sig
-  include BASIC_RULIFY
-  val rule_format: 'a attribute
-  val rule_format_no_asm: 'a attribute
-  val setup: (theory -> theory) list
-end;
-
-functor RulifyFun(val make_meta: thm -> thm val full_make_meta: thm -> thm): RULIFY =
-struct
-
-
-(* rulify *)
-
-val tune = Drule.zero_var_indexes o Drule.strip_shyps_warning o Drule.forall_elim_vars_safe;
-
-val rulify = tune o full_make_meta;
-val rulify_no_asm = tune o make_meta;
-
-
-(* attributes *)
-
-fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
-fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
-
-fun rule_format_att x = Attrib.syntax
-  (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rule_format_no_asm || Scan.succeed rule_format)) x;
-
-
-(* qed commands *)
-
-fun qed_spec_mp name = ThmDatabase.ml_store_thm (name, rulify_no_asm (Goals.result ()));
-
-fun qed_goal_spec_mp name thy s p =
-  ThmDatabase.bind_thm (name, rulify_no_asm (Goals.prove_goal thy s p));
-
-fun qed_goalw_spec_mp name thy defs s p =
-  ThmDatabase.bind_thm (name, rulify_no_asm (Goals.prove_goalw thy defs s p));
-
-
-(* theory setup *)
-
-val setup =
- [Attrib.add_attributes
-  [("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")]];
-
-end;