--- a/src/HOL/Code_Evaluation.thy Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy Tue Nov 10 18:32:41 2009 +0100
@@ -64,7 +64,7 @@
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
in
thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
+ |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
|> snd
--- a/src/HOL/HOL.thy Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/HOL.thy Tue Nov 10 18:32:41 2009 +0100
@@ -2003,16 +2003,6 @@
quickcheck_params [size = 5, iterations = 50]
-ML {*
-structure Quickcheck_RecFun_Simps = Named_Thms
-(
- val name = "quickcheck_recfun_simp"
- val description = "simplification rules of recursive functions as needed by Quickcheck"
-)
-*}
-
-setup Quickcheck_RecFun_Simps.setup
-
subsubsection {* Nitpick setup *}
--- a/src/HOL/Library/Float.thy Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Library/Float.thy Tue Nov 10 18:32:41 2009 +0100
@@ -1378,8 +1378,8 @@
assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y"
proof -
- have "?lb \<le> ?ub" by (auto!)
- have "0 \<le> ?lb" and "?lb \<noteq> 0" by (auto!)
+ have "?lb \<le> ?ub" using assms by auto
+ have "0 \<le> ?lb" and "?lb \<noteq> 0" using assms by auto
have "?k * y \<le> ?x" using assms by auto
also have "\<dots> \<le> ?x / ?lb * ?ub" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?lb` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?lb \<noteq> 0`])
also have "\<dots> \<le> real (ceiling_fl (float_divr prec x lb)) * ?ub" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divr ceiling_fl)
@@ -1390,8 +1390,8 @@
assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
proof -
- have "?lb \<le> ?ub" by (auto!)
- hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" by (auto!)
+ have "?lb \<le> ?ub" using assms by auto
+ hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" using assms by auto
have "real (floor_fl (float_divl prec x ub)) * ?lb \<le> ?x / ?ub * ?lb" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divl floor_fl)
also have "\<dots> \<le> ?x" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?ub` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?ub \<noteq> 0`])
also have "\<dots> \<le> ?k * y" using assms by auto
--- a/src/HOL/Nominal/nominal_permeq.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Tue Nov 10 18:32:41 2009 +0100
@@ -397,11 +397,8 @@
Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
val perm_simp_meth =
- Args.bang_facts -- Scan.lift perm_simp_options --|
- Method.sections (Simplifier.simp_modifiers') >>
- (fn (prems, tac) => fn ctxt => METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN'
- (CHANGED_PROP oo tac) (simpset_of ctxt))));
+ Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >>
+ (fn tac => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o tac (simpset_of ctxt)));
(* setup so that the simpset is used which is active at the moment when the tactic is called *)
fun local_simp_meth_setup tac =
--- a/src/HOL/Statespace/state_space.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Tue Nov 10 18:32:41 2009 +0100
@@ -349,7 +349,7 @@
fun add_declaration name decl thy =
thy
- |> TheoryTarget.init name
+ |> Theory_Target.init name
|> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
|> LocalTheory.exit_global;
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Nov 10 18:32:41 2009 +0100
@@ -411,7 +411,7 @@
#> fold_rev Code.add_eqn thms);
in
thy
- |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq])
+ |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
|> fold_map add_def dtcos
|-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
(fn _ => fn def_thms => tac def_thms) def_thms)
--- a/src/HOL/Tools/Function/function.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML Tue Nov 10 18:32:41 2009 +0100
@@ -37,8 +37,7 @@
val simp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
Code.add_default_eqn_attribute,
- Nitpick_Simps.add,
- Quickcheck_RecFun_Simps.add]
+ Nitpick_Simps.add]
val psimp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
--- a/src/HOL/Tools/Function/size.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML Tue Nov 10 18:32:41 2009 +0100
@@ -144,7 +144,7 @@
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
(map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
- ||> TheoryTarget.instantiation
+ ||> Theory_Target.instantiation
(map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
||>> fold_map define_overloaded
(def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
--- a/src/HOL/Tools/arith_data.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML Tue Nov 10 18:32:41 2009 +0100
@@ -65,8 +65,8 @@
val setup =
Arith_Facts.setup #>
Method.setup @{binding arith}
- (Args.bang_facts >> (fn prems => fn ctxt =>
- METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+ (Scan.succeed (fn ctxt =>
+ METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts)
THEN' verbose_arith_tac ctxt))))
"various arithmetic decision procedures";
--- a/src/HOL/Tools/inductive.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Nov 10 18:32:41 2009 +0100
@@ -896,7 +896,7 @@
let
val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
val ctxt' = thy
- |> TheoryTarget.init NONE
+ |> Theory_Target.init NONE
|> LocalTheory.set_group group
|> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
|> LocalTheory.exit;
--- a/src/HOL/Tools/lin_arith.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Tue Nov 10 18:32:41 2009 +0100
@@ -924,9 +924,9 @@
Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
"declaration of split rules for arithmetic procedure" #>
Method.setup @{binding linarith}
- (Args.bang_facts >> (fn prems => fn ctxt =>
+ (Scan.succeed (fn ctxt =>
METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+ HEADGOAL (Method.insert_tac (Arith_Data.get_arith_facts ctxt @ facts)
THEN' tac ctxt)))) "linear arithmetic" #>
Arith_Data.add_tactic "linear arithmetic" gen_tac;
--- a/src/HOL/Tools/primrec.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/primrec.ML Tue Nov 10 18:32:41 2009 +0100
@@ -270,9 +270,9 @@
val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
fun attr_bindings prefix = map (fn ((b, attrs), _) =>
(Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
- fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
- map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]);
+ fun simp_attr_binding prefix =
+ (Binding.qualify true prefix (Binding.name "simps"),
+ map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
in
lthy
|> set_group ? LocalTheory.set_group (serial ())
@@ -293,14 +293,14 @@
fun add_primrec_global fixes specs thy =
let
- val lthy = TheoryTarget.init NONE thy;
+ val lthy = Theory_Target.init NONE thy;
val (simps, lthy') = add_primrec fixes specs lthy;
val simps' = ProofContext.export lthy' lthy simps;
in (simps', LocalTheory.exit_global lthy') end;
fun add_primrec_overloaded ops fixes specs thy =
let
- val lthy = TheoryTarget.overloading ops thy;
+ val lthy = Theory_Target.overloading ops thy;
val (simps, lthy') = add_primrec fixes specs lthy;
val simps' = ProofContext.export lthy' lthy simps;
in (simps', LocalTheory.exit_global lthy') end;
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Nov 10 18:32:41 2009 +0100
@@ -82,7 +82,7 @@
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+ |> Theory_Target.instantiation ([tyco], vs, @{sort random})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
|> snd
@@ -216,8 +216,7 @@
|-> (fn proto_simps => prove_simps proto_simps)
|-> (fn simps => LocalTheory.note Thm.generatedK ((b,
Code.add_default_eqn_attrib :: map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]),
- simps))
+ [Simplifier.simp_add, Nitpick_Simps.add]), simps))
|> snd
end
@@ -301,7 +300,7 @@
(HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
in
thy
- |> TheoryTarget.instantiation (tycos, vs, @{sort random})
+ |> Theory_Target.instantiation (tycos, vs, @{sort random})
|> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
--- a/src/HOL/Tools/recdef.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/recdef.ML Tue Nov 10 18:32:41 2009 +0100
@@ -201,8 +201,9 @@
tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
congs wfs name R eqs;
val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
- val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Simps.add,
- Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
+ val simp_att =
+ if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]
+ else [];
val ((simps' :: rules', [induct']), thy) =
thy
--- a/src/HOL/Tools/typecopy.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML Tue Nov 10 18:32:41 2009 +0100
@@ -113,7 +113,7 @@
thy
|> Code.add_datatype [constr]
|> Code.add_eqn proj_eq
- |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
+ |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition
(NONE, (Attrib.empty_binding, eq)))
--- a/src/HOL/Transcendental.thy Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Transcendental.thy Tue Nov 10 18:32:41 2009 +0100
@@ -25,7 +25,7 @@
"(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
- del: setsum_op_ivl_Suc cong: strong_setsum_cong)
+ del: setsum_op_ivl_Suc)
lemma lemma_realpow_diff_sumr2:
fixes y :: "'a::{comm_ring,monoid_mult}" shows
@@ -1981,11 +1981,11 @@
lemma cos_monotone_0_pi: assumes "0 \<le> y" and "y < x" and "x \<le> pi"
shows "cos x < cos y"
proof -
- have "- (x - y) < 0" by (auto!)
+ have "- (x - y) < 0" using assms by auto
from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z" by auto
- hence "0 < z" and "z < pi" by (auto!)
+ hence "0 < z" and "z < pi" using assms by auto
hence "0 < sin z" using sin_gt_zero_pi by auto
hence "cos x - cos y < 0" unfolding cos_diff minus_mult_commute[symmetric] using `- (x - y) < 0` by (rule mult_pos_neg2)
thus ?thesis by auto
@@ -2002,7 +2002,7 @@
lemma cos_monotone_minus_pi_0: assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
shows "cos y < cos x"
proof -
- have "0 \<le> -x" and "-x < -y" and "-y \<le> pi" by (auto!)
+ have "0 \<le> -x" and "-x < -y" and "-y \<le> pi" using assms by auto
from cos_monotone_0_pi[OF this]
show ?thesis unfolding cos_minus .
qed
@@ -2017,7 +2017,8 @@
lemma sin_monotone_2pi': assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2" shows "sin y \<le> sin x"
proof -
- have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi" using pi_ge_two by (auto!)
+ have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
+ using pi_ge_two and assms by auto
from cos_monotone_0_pi'[OF this] show ?thesis unfolding minus_sin_cos_eq[symmetric] by auto
qed
@@ -2179,14 +2180,14 @@
have "\<forall> x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse (cos x'^2)"
proof (rule allI, rule impI)
fix x' :: real assume "y \<le> x' \<and> x' \<le> x"
- hence "-(pi/2) < x'" and "x' < pi/2" by (auto!)
+ hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
from cos_gt_zero_pi[OF this]
have "cos x' \<noteq> 0" by auto
thus "DERIV tan x' :> inverse (cos x'^2)" by (rule DERIV_tan)
qed
from MVT2[OF `y < x` this]
obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<twosuperior>)" by auto
- hence "- (pi / 2) < z" and "z < pi / 2" by (auto!)
+ hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
hence "0 < cos z" using cos_gt_zero_pi by auto
hence inv_pos: "0 < inverse ((cos z)\<twosuperior>)" by auto
have "0 < x - y" using `y < x` by auto
--- a/src/HOL/Typerep.thy Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Typerep.thy Tue Nov 10 18:32:41 2009 +0100
@@ -50,7 +50,7 @@
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
+ |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
|> snd
--- a/src/HOLCF/Tools/pcpodef.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Tue Nov 10 18:32:41 2009 +0100
@@ -75,7 +75,7 @@
val ((_, {type_definition, set_def, ...}), thy2) = thy1
|> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
val lthy3 = thy2
- |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
+ |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
val below_def' = Syntax.check_term lthy3 below_def;
val ((_, (_, below_definition')), lthy4) = lthy3
|> Specification.definition (NONE,
--- a/src/Pure/General/symbol.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/General/symbol.ML Tue Nov 10 18:32:41 2009 +0100
@@ -18,7 +18,6 @@
val is_symbolic: symbol -> bool
val is_printable: symbol -> bool
val is_utf8_trailer: symbol -> bool
- val name_of: symbol -> string
val eof: symbol
val is_eof: symbol -> bool
val not_eof: symbol -> bool
@@ -137,10 +136,6 @@
fun is_regular s =
not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
-fun name_of s = if is_symbolic s
- then (unsuffix ">" o unprefix "\\<") s
- else error (malformed_msg s);
-
(* ascii symbols *)
--- a/src/Pure/Isar/args.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/args.ML Tue Nov 10 18:32:41 2009 +0100
@@ -223,7 +223,7 @@
val bang_facts = Scan.peek (fn context =>
P.position ($$$ "!") >> (fn (_, pos) =>
- (warning ("use of prems in proof method" ^ Position.str_of pos);
+ (legacy_feature ("use of cumulative prems (!) in proof method" ^ Position.str_of pos);
Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
val from_to =
--- a/src/Pure/Isar/class.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/class.ML Tue Nov 10 18:32:41 2009 +0100
@@ -290,7 +290,7 @@
Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
(*FIXME should not modify base_morph, although admissible*)
#> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
- |> TheoryTarget.init (SOME class)
+ |> Theory_Target.init (SOME class)
|> pair class
end;
@@ -310,7 +310,7 @@
let
val thy = ProofContext.theory_of lthy;
val proto_sup = prep_class thy raw_sup;
- val proto_sub = case TheoryTarget.peek lthy
+ val proto_sub = case Theory_Target.peek lthy
of {is_class = false, ...} => error "Not in a class context"
| {target, ...} => target;
val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
@@ -323,7 +323,7 @@
fun after_qed some_wit =
ProofContext.theory (register_subclass (sub, sup)
some_dep_morph some_wit export)
- #> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
+ #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
in do_proof after_qed some_prop goal_ctxt end;
fun user_proof after_qed some_prop =
--- a/src/Pure/Isar/expression.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/expression.ML Tue Nov 10 18:32:41 2009 +0100
@@ -774,7 +774,7 @@
val loc_ctxt = thy'
|> Locale.register_locale binding (extraTs, params)
(asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
- |> TheoryTarget.init (SOME name)
+ |> Theory_Target.init (SOME name)
|> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
in (name, loc_ctxt) end;
@@ -842,7 +842,7 @@
fun gen_sublocale prep_expr intern raw_target expression thy =
let
val target = intern thy raw_target;
- val target_ctxt = TheoryTarget.init (SOME target) thy;
+ val target_ctxt = Theory_Target.init (SOME target) thy;
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
fun after_qed witss = ProofContext.theory
(fold (fn ((dep, morph), wits) => Locale.add_dependency
--- a/src/Pure/Isar/isar_syn.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Nov 10 18:32:41 2009 +0100
@@ -390,7 +390,7 @@
val _ =
OuterSyntax.command "context" "enter local theory context" K.thy_decl
(P.name --| P.begin >> (fn name =>
- Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.context name)));
+ Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name)));
(* locales *)
@@ -452,7 +452,7 @@
OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
(P.multi_arity --| P.begin
>> (fn arities => Toplevel.print o
- Toplevel.begin_local_theory true (TheoryTarget.instantiation_cmd arities)));
+ Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
val _ =
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
@@ -470,7 +470,7 @@
Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
>> P.triple1) --| P.begin
>> (fn operations => Toplevel.print o
- Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));
+ Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
(* code generation *)
--- a/src/Pure/Isar/theory_target.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Tue Nov 10 18:32:41 2009 +0100
@@ -19,7 +19,7 @@
val overloading_cmd: (string * string * bool) list -> theory -> local_theory
end;
-structure TheoryTarget: THEORY_TARGET =
+structure Theory_Target: THEORY_TARGET =
struct
(* context data *)
--- a/src/Pure/Isar/toplevel.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Tue Nov 10 18:32:41 2009 +0100
@@ -103,7 +103,7 @@
type generic_theory = Context.generic; (*theory or local_theory*)
-val loc_init = TheoryTarget.context;
+val loc_init = Theory_Target.context;
val loc_exit = LocalTheory.exit_global;
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
@@ -192,7 +192,7 @@
(* print state *)
-val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I;
+val pretty_context = LocalTheory.pretty o Context.cases (Theory_Target.init NONE) I;
fun print_state_context state =
(case try node_of state of
--- a/src/Pure/name.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/name.ML Tue Nov 10 18:32:41 2009 +0100
@@ -152,7 +152,8 @@
| desymbolize upper s =
let
val xs as (x :: _) = Symbol.explode s;
- val ys = if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
+ val ys =
+ if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
else "x" :: xs;
fun is_valid x =
Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "'";
@@ -161,15 +162,17 @@
| sep xs = "_" :: xs;
fun desep ("_" :: xs) = xs
| desep xs = xs;
- fun desymb x xs = if is_valid x
- then x :: xs
- else if Symbol.is_symbolic x
- then "_" :: explode (Symbol.name_of x) @ sep xs
+ fun desymb x xs =
+ if is_valid x then x :: xs
else
- sep xs
- fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
- else (if forall Symbol.is_ascii_upper cs
- then map else nth_map 0) Symbol.to_ascii_lower cs;
+ (case Symbol.decode x of
+ Symbol.Sym name => "_" :: explode name @ sep xs
+ | _ => sep xs);
+ fun upper_lower cs =
+ if upper then nth_map 0 Symbol.to_ascii_upper cs
+ else
+ (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
+ Symbol.to_ascii_lower cs;
in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
end;
--- a/src/Pure/simplifier.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/simplifier.ML Tue Nov 10 18:32:41 2009 +0100
@@ -189,8 +189,7 @@
in Variable.export_terms ctxt' lthy lhss' end
|> map (Thm.cterm_of (ProofContext.theory_of lthy)),
proc = proc,
- identifier = identifier}
- |> morph_simproc (LocalTheory.target_morphism lthy);
+ identifier = identifier};
in
lthy |> LocalTheory.declaration false (fn phi =>
let
--- a/src/Tools/intuitionistic.ML Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Tools/intuitionistic.ML Tue Nov 10 18:32:41 2009 +0100
@@ -87,11 +87,9 @@
fun method_setup name =
Method.setup name
- (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
- Method.sections modifiers >>
- (fn (prems, n) => fn ctxt => METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN'
- ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))))
+ (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
+ (fn opt_lim => fn ctxt =>
+ SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
"intuitionistic proof search";
end;