--- a/src/HOL/Modelcheck/CTL.thy Sat Aug 18 17:42:38 2007 +0200
+++ b/src/HOL/Modelcheck/CTL.thy Sat Aug 18 17:42:39 2007 +0200
@@ -17,6 +17,4 @@
EG ::"['a trans,'a pred]=> 'a pred"
"EG N f == nu (% Q. % u.(f u & CEX N Q u))"
-ML {* use_legacy_bindings (the_context ()) *}
-
end
--- a/src/HOL/Modelcheck/MuCalculus.thy Sat Aug 18 17:42:38 2007 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.thy Sat Aug 18 17:42:39 2007 +0200
@@ -24,6 +24,4 @@
nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
"nu f == Charfun(gfp(Collect o f o Charfun))"
-ML {* use_legacy_bindings (the_context ()) *}
-
end
--- a/src/HOL/Subst/Unify.thy Sat Aug 18 17:42:38 2007 +0200
+++ b/src/HOL/Subst/Unify.thy Sat Aug 18 17:42:39 2007 +0200
@@ -178,16 +178,18 @@
| Some sigma => Some (theta \<lozenge> sigma)))"
by (simp add: unify_tc2 unify_simps0 split add: option.split)
-text{*The ML version had this, but it can't be used: we get
-*** exception THM raised: transfer: not a super theory
-All we can do is state the desired induction rule in full and prove it.*}
-ML{*
-bind_thm ("unify_induct",
- rule_by_tactic
- (ALLGOALS (full_simp_tac (simpset() addsimps [thm"unify_tc2"])))
- (thm"unify_induct0"));
-*}
-
+lemma unify_induct:
+ "(\<And>m n. P (Const m) (Const n)) \<Longrightarrow>
+ (\<And>m M N. P (Const m) (Comb M N)) \<Longrightarrow>
+ (\<And>m v. P (Const m) (Var v)) \<Longrightarrow>
+ (\<And>v M. P (Var v) M) \<Longrightarrow>
+ (\<And>M N x. P (Comb M N) (Const x)) \<Longrightarrow>
+ (\<And>M N v. P (Comb M N) (Var v)) \<Longrightarrow>
+ (\<And>M1 N1 M2 N2.
+ \<forall>theta. unify (M1, M2) = Some theta \<longrightarrow> P (N1 \<lhd> theta) (N2 \<lhd> theta) \<Longrightarrow>
+ P M1 M2 \<Longrightarrow> P (Comb M1 N1) (Comb M2 N2)) \<Longrightarrow>
+ P u v"
+by (rule unify_induct0) (simp_all add: unify_tc2)
text{*Correctness. Notice that idempotence is not needed to prove that the
algorithm terminates and is not needed to prove the algorithm correct, if you
--- a/src/HOLCF/FOCUS/Fstream.thy Sat Aug 18 17:42:38 2007 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Sat Aug 18 17:42:39 2007 +0200
@@ -150,8 +150,6 @@
section "slen"
-(*bind_thm("slen_empty", slen_empty);*)
-
lemma slen_fscons: "#(m~> s) = iSuc (#s)"
by (simp add: fscons_def)
--- a/src/HOLCF/IOA/NTP/Impl.thy Sat Aug 18 17:42:38 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.thy Sat Aug 18 17:42:39 2007 +0200
@@ -357,11 +357,9 @@
text {* rebind them *}
-ML_setup {*
-bind_thm ("inv1", rewrite_rule [thm "Impl.inv1_def"] (thm "inv1" RS thm "invariantE"));
-bind_thm ("inv2", rewrite_rule [thm "Impl.inv2_def"] (thm "inv2" RS thm "invariantE"));
-bind_thm ("inv3", rewrite_rule [thm "Impl.inv3_def"] (thm "inv3" RS thm "invariantE"));
-bind_thm ("inv4", rewrite_rule [thm "Impl.inv4_def"] (thm "inv4" RS thm "invariantE"));
-*}
+lemmas inv1 = inv1 [THEN invariantE, unfolded inv1_def]
+ and inv2 = inv2 [THEN invariantE, unfolded inv2_def]
+ and inv3 = inv3 [THEN invariantE, unfolded inv3_def]
+ and inv4 = inv4 [THEN invariantE, unfolded inv4_def]
end
--- a/src/ZF/UNITY/Comp.thy Sat Aug 18 17:42:38 2007 +0200
+++ b/src/ZF/UNITY/Comp.thy Sat Aug 18 17:42:39 2007 +0200
@@ -136,8 +136,6 @@
apply (auto simp add: constrains_def component_eq_subset)
done
-(* Used in Guar.thy to show that programs are partially ordered*)
-(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*)
(*** preserves ***)
@@ -337,57 +335,4 @@
apply (blast intro: constrains_weaken)
done
-ML
-{*
-val component_of_def = thm "component_of_def";
-val component_def = thm "component_def";
-
-val componentI = thm "componentI";
-val component_eq_subset = thm "component_eq_subset";
-val component_SKIP = thm "component_SKIP";
-val component_refl = thm "component_refl";
-val SKIP_minimal = thm "SKIP_minimal";
-val component_Join1 = thm "component_Join1";
-val component_Join2 = thm "component_Join2";
-val Join_absorb1 = thm "Join_absorb1";
-val Join_absorb2 = thm "Join_absorb2";
-val JN_component_iff = thm "JN_component_iff";
-val component_JN = thm "component_JN";
-val component_trans = thm "component_trans";
-val component_antisym = thm "component_antisym";
-val Join_component_iff = thm "Join_component_iff";
-val component_constrains = thm "component_constrains";
-val preserves_is_safety_prop = thm "preserves_is_safety_prop";
-val preservesI = thm "preservesI";
-val preserves_imp_eq = thm "preserves_imp_eq";
-val Join_preserves = thm "Join_preserves";
-val JN_preserves = thm "JN_preserves";
-val SKIP_preserves = thm "SKIP_preserves";
-val fun_pair_apply = thm "fun_pair_apply";
-val preserves_fun_pair = thm "preserves_fun_pair";
-val preserves_fun_pair_iff = thm "preserves_fun_pair_iff";
-val fun_pair_comp_distrib = thm "fun_pair_comp_distrib";
-val comp_apply = thm "comp_apply";
-val preserves_type = thm "preserves_type";
-val preserves_into_program = thm "preserves_into_program";
-val subset_preserves_comp = thm "subset_preserves_comp";
-val imp_preserves_comp = thm "imp_preserves_comp";
-val preserves_subset_stable = thm "preserves_subset_stable";
-val preserves_imp_stable = thm "preserves_imp_stable";
-val preserves_imp_increasing = thm "preserves_imp_increasing";
-val preserves_id_subset_stable = thm "preserves_id_subset_stable";
-val preserves_id_imp_stable = thm "preserves_id_imp_stable";
-val component_of_imp_component = thm "component_of_imp_component";
-val component_of_refl = thm "component_of_refl";
-val component_of_SKIP = thm "component_of_SKIP";
-val component_of_trans = thm "component_of_trans";
-val localize_Init_eq = thm "localize_Init_eq";
-val localize_Acts_eq = thm "localize_Acts_eq";
-val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
-val stable_localTo_stable2 = thm "stable_localTo_stable2";
-val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
-val Constrains_UN_left = thm "Constrains_UN_left";
-val stable_Join_Stable = thm "stable_Join_Stable";
-*}
-
end