# HG changeset patch # User wenzelm # Date 1187451759 -7200 # Node ID a207114007c62317903d0fbe94a9c2c33de7e769 # Parent 3e9d3ba894b832c6cd594c9e688e8af18aafb5be removed obsolete ML bindings; diff -r 3e9d3ba894b8 -r a207114007c6 src/HOL/Modelcheck/CTL.thy --- 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 diff -r 3e9d3ba894b8 -r a207114007c6 src/HOL/Modelcheck/MuCalculus.thy --- 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 diff -r 3e9d3ba894b8 -r a207114007c6 src/HOL/Subst/Unify.thy --- 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 \ 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: + "(\m n. P (Const m) (Const n)) \ + (\m M N. P (Const m) (Comb M N)) \ + (\m v. P (Const m) (Var v)) \ + (\v M. P (Var v) M) \ + (\M N x. P (Comb M N) (Const x)) \ + (\M N v. P (Comb M N) (Var v)) \ + (\M1 N1 M2 N2. + \theta. unify (M1, M2) = Some theta \ P (N1 \ theta) (N2 \ theta) \ + P M1 M2 \ P (Comb M1 N1) (Comb M2 N2)) \ + 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 diff -r 3e9d3ba894b8 -r a207114007c6 src/HOLCF/FOCUS/Fstream.thy --- 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) diff -r 3e9d3ba894b8 -r a207114007c6 src/HOLCF/IOA/NTP/Impl.thy --- 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 diff -r 3e9d3ba894b8 -r a207114007c6 src/ZF/UNITY/Comp.thy --- 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