1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 07 11:57:16 2010 +0100
1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 07 12:19:47 2010 +0100
1.3 @@ -87,8 +87,8 @@
1.4 | NONE =>
1.5 let
1.6 val args = Name.variant_list [] (replicate arity "'")
1.7 - val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args,
1.8 - mk_syntax name arity) thy
1.9 + val (T, thy') =
1.10 + Object_Logic.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
1.11 val type_name = fst (Term.dest_Type T)
1.12 in (((name, type_name), log_new name type_name), thy') end)
1.13 end
2.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Mar 07 11:57:16 2010 +0100
2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Mar 07 12:19:47 2010 +0100
2.3 @@ -3098,7 +3098,7 @@
2.4 struct
2.5
2.6 fun frpar_tac T ps ctxt i =
2.7 - (ObjectLogic.full_atomize_tac i)
2.8 + Object_Logic.full_atomize_tac i
2.9 THEN (fn st =>
2.10 let
2.11 val g = List.nth (cprems_of st, i - 1)
2.12 @@ -3108,7 +3108,7 @@
2.13 in rtac (th RS iffD2) i st end);
2.14
2.15 fun frpar2_tac T ps ctxt i =
2.16 - (ObjectLogic.full_atomize_tac i)
2.17 + Object_Logic.full_atomize_tac i
2.18 THEN (fn st =>
2.19 let
2.20 val g = List.nth (cprems_of st, i - 1)
3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Mar 07 11:57:16 2010 +0100
3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Mar 07 12:19:47 2010 +0100
3.3 @@ -66,7 +66,7 @@
3.4 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
3.5
3.6
3.7 -fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
3.8 +fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
3.9 let
3.10 val g = List.nth (prems_of st, i - 1)
3.11 val thy = ProofContext.theory_of ctxt
4.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun Mar 07 11:57:16 2010 +0100
4.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun Mar 07 12:19:47 2010 +0100
4.3 @@ -73,7 +73,7 @@
4.4
4.5
4.6 fun linr_tac ctxt q =
4.7 - ObjectLogic.atomize_prems_tac
4.8 + Object_Logic.atomize_prems_tac
4.9 THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
4.10 THEN' SUBGOAL (fn (g, i) =>
4.11 let
5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML Sun Mar 07 11:57:16 2010 +0100
5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Mar 07 12:19:47 2010 +0100
5.3 @@ -88,7 +88,7 @@
5.4
5.5
5.6 fun mir_tac ctxt q i =
5.7 - ObjectLogic.atomize_prems_tac i
5.8 + Object_Logic.atomize_prems_tac i
5.9 THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
5.10 THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
5.11 THEN (fn st =>
6.1 --- a/src/HOL/HOL.thy Sun Mar 07 11:57:16 2010 +0100
6.2 +++ b/src/HOL/HOL.thy Sun Mar 07 12:19:47 2010 +0100
6.3 @@ -44,7 +44,7 @@
6.4
6.5 classes type
6.6 defaultsort type
6.7 -setup {* ObjectLogic.add_base_sort @{sort type} *}
6.8 +setup {* Object_Logic.add_base_sort @{sort type} *}
6.9
6.10 arities
6.11 "fun" :: (type, type) type
7.1 --- a/src/HOL/Library/Efficient_Nat.thy Sun Mar 07 11:57:16 2010 +0100
7.2 +++ b/src/HOL/Library/Efficient_Nat.thy Sun Mar 07 12:19:47 2010 +0100
7.3 @@ -181,7 +181,7 @@
7.4 | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
7.5 | find_var _ = NONE;
7.6 fun find_thm th =
7.7 - let val th' = Conv.fconv_rule ObjectLogic.atomize th
7.8 + let val th' = Conv.fconv_rule Object_Logic.atomize th
7.9 in Option.map (pair (th, th')) (find_var (prop_of th')) end
7.10 in
7.11 case get_first find_thm thms of
7.12 @@ -189,7 +189,7 @@
7.13 | SOME ((th, th'), (Sucv, v)) =>
7.14 let
7.15 val cert = cterm_of (Thm.theory_of_thm th);
7.16 - val th'' = ObjectLogic.rulify (Thm.implies_elim
7.17 + val th'' = Object_Logic.rulify (Thm.implies_elim
7.18 (Conv.fconv_rule (Thm.beta_conversion true)
7.19 (Drule.instantiate' []
7.20 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
8.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sun Mar 07 11:57:16 2010 +0100
8.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sun Mar 07 12:19:47 2010 +0100
8.3 @@ -1431,7 +1431,7 @@
8.4 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
8.5
8.6 fun sos_tac print_cert prover ctxt =
8.7 - ObjectLogic.full_atomize_tac THEN'
8.8 + Object_Logic.full_atomize_tac THEN'
8.9 elim_denom_tac ctxt THEN'
8.10 core_sos_tac print_cert prover ctxt;
8.11
9.1 --- a/src/HOL/Library/normarith.ML Sun Mar 07 11:57:16 2010 +0100
9.2 +++ b/src/HOL/Library/normarith.ML Sun Mar 07 12:19:47 2010 +0100
9.3 @@ -410,7 +410,7 @@
9.4
9.5 fun norm_arith_tac ctxt =
9.6 clarify_tac HOL_cs THEN'
9.7 - ObjectLogic.full_atomize_tac THEN'
9.8 + Object_Logic.full_atomize_tac THEN'
9.9 CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
9.10
9.11 end;
10.1 --- a/src/HOL/Mutabelle/mutabelle.ML Sun Mar 07 11:57:16 2010 +0100
10.2 +++ b/src/HOL/Mutabelle/mutabelle.ML Sun Mar 07 12:19:47 2010 +0100
10.3 @@ -494,7 +494,7 @@
10.4 fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
10.5 | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
10.6
10.7 -fun preprocess thy insts t = ObjectLogic.atomize_term thy
10.8 +fun preprocess thy insts t = Object_Logic.atomize_term thy
10.9 (map_types (inst_type insts) (freeze t));
10.10
10.11 fun is_executable thy insts th =
11.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 07 11:57:16 2010 +0100
11.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 07 12:19:47 2010 +0100
11.3 @@ -91,7 +91,7 @@
11.4 fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
11.5 | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
11.6
11.7 -fun preprocess thy insts t = ObjectLogic.atomize_term thy
11.8 +fun preprocess thy insts t = Object_Logic.atomize_term thy
11.9 (map_types (inst_type insts) (Mutabelle.freeze t));
11.10
11.11 fun invoke_quickcheck quickcheck_generator thy t =
12.1 --- a/src/HOL/NSA/transfer.ML Sun Mar 07 11:57:16 2010 +0100
12.2 +++ b/src/HOL/NSA/transfer.ML Sun Mar 07 12:19:47 2010 +0100
12.3 @@ -63,7 +63,7 @@
12.4 val u = unstar_term consts t'
12.5 val tac =
12.6 rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
12.7 - ALLGOALS ObjectLogic.full_atomize_tac THEN
12.8 + ALLGOALS Object_Logic.full_atomize_tac THEN
12.9 match_tac [transitive_thm] 1 THEN
12.10 resolve_tac [@{thm transfer_start}] 1 THEN
12.11 REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
13.1 --- a/src/HOL/Nominal/nominal_datatype.ML Sun Mar 07 11:57:16 2010 +0100
13.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Sun Mar 07 12:19:47 2010 +0100
13.3 @@ -1074,7 +1074,7 @@
13.4 (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
13.5 (fn {prems, ...} => EVERY
13.6 [rtac indrule_lemma' 1,
13.7 - (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
13.8 + (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
13.9 EVERY (map (fn (prem, r) => (EVERY
13.10 [REPEAT (eresolve_tac Abs_inverse_thms' 1),
13.11 simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
14.1 --- a/src/HOL/Tools/Datatype/datatype.ML Sun Mar 07 11:57:16 2010 +0100
14.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Sun Mar 07 12:19:47 2010 +0100
14.3 @@ -417,7 +417,7 @@
14.4
14.5 val inj_thm = Skip_Proof.prove_global thy5 [] []
14.6 (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
14.7 - [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
14.8 + [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
14.9 REPEAT (EVERY
14.10 [rtac allI 1, rtac impI 1,
14.11 exh_tac (exh_thm_of dt_info) 1,
14.12 @@ -443,7 +443,7 @@
14.13 val elem_thm =
14.14 Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
14.15 (fn _ =>
14.16 - EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
14.17 + EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
14.18 rewrite_goals_tac rewrites,
14.19 REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
14.20 ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
14.21 @@ -479,7 +479,7 @@
14.22 val iso_thms = if length descr = 1 then [] else
14.23 drop (length newTs) (split_conj_thm
14.24 (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
14.25 - [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
14.26 + [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
14.27 REPEAT (rtac TrueI 1),
14.28 rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
14.29 symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
14.30 @@ -617,7 +617,7 @@
14.31 (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
14.32 (fn {prems, ...} => EVERY
14.33 [rtac indrule_lemma' 1,
14.34 - (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
14.35 + (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
14.36 EVERY (map (fn (prem, r) => (EVERY
14.37 [REPEAT (eresolve_tac Abs_inverse_thms 1),
14.38 simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
15.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Mar 07 11:57:16 2010 +0100
15.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Mar 07 12:19:47 2010 +0100
15.3 @@ -209,7 +209,7 @@
15.4 val induct' = cterm_instantiate ((map cert induct_Ps) ~~
15.5 (map cert insts)) induct;
15.6 val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
15.7 - (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
15.8 + (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
15.9 THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
15.10
15.11 in split_conj_thm (Skip_Proof.prove_global thy1 [] []
16.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sun Mar 07 11:57:16 2010 +0100
16.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sun Mar 07 12:19:47 2010 +0100
16.3 @@ -115,7 +115,7 @@
16.4 (fn prems =>
16.5 [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
16.6 rtac (cterm_instantiate inst induct) 1,
16.7 - ALLGOALS ObjectLogic.atomize_prems_tac,
16.8 + ALLGOALS Object_Logic.atomize_prems_tac,
16.9 rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
16.10 REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
16.11 REPEAT (etac allE i) THEN atac i)) 1)]);
17.1 --- a/src/HOL/Tools/Function/induction_schema.ML Sun Mar 07 11:57:16 2010 +0100
17.2 +++ b/src/HOL/Tools/Function/induction_schema.ML Sun Mar 07 12:19:47 2010 +0100
17.3 @@ -195,7 +195,7 @@
17.4 |> fold_rev (curry Logic.mk_implies) Cs
17.5 |> fold_rev (Logic.all o Free) ws
17.6 |> term_conv thy ind_atomize
17.7 - |> ObjectLogic.drop_judgment thy
17.8 + |> Object_Logic.drop_judgment thy
17.9 |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
17.10 in
17.11 SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
18.1 --- a/src/HOL/Tools/Function/termination.ML Sun Mar 07 11:57:16 2010 +0100
18.2 +++ b/src/HOL/Tools/Function/termination.ML Sun Mar 07 12:19:47 2010 +0100
18.3 @@ -282,7 +282,7 @@
18.4 let
18.5 val (vars, prems, lhs, rhs) = dest_term ineq
18.6 in
18.7 - mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
18.8 + mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
18.9 end
18.10
18.11 val relation =
19.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Mar 07 11:57:16 2010 +0100
19.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Mar 07 12:19:47 2010 +0100
19.3 @@ -967,10 +967,11 @@
19.4 (semiring_normalize_wrapper ctxt res)) form));
19.5
19.6 fun ring_tac add_ths del_ths ctxt =
19.7 - ObjectLogic.full_atomize_tac
19.8 - THEN' asm_full_simp_tac (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
19.9 + Object_Logic.full_atomize_tac
19.10 + THEN' asm_full_simp_tac
19.11 + (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
19.12 THEN' CSUBGOAL (fn (p, i) =>
19.13 - rtac (let val form = (ObjectLogic.dest_judgment p)
19.14 + rtac (let val form = Object_Logic.dest_judgment p
19.15 in case get_ring_ideal_convs ctxt form of
19.16 NONE => reflexive form
19.17 | SOME thy => #ring_conv thy form
19.18 @@ -1008,7 +1009,7 @@
19.19 end
19.20 in
19.21 clarify_tac @{claset} i
19.22 - THEN ObjectLogic.full_atomize_tac i
19.23 + THEN Object_Logic.full_atomize_tac i
19.24 THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i
19.25 THEN clarify_tac @{claset} i
19.26 THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
20.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Sun Mar 07 11:57:16 2010 +0100
20.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Sun Mar 07 12:19:47 2010 +0100
20.3 @@ -298,7 +298,7 @@
20.4 | card (Type ("*", [T1, T2])) = card T1 * card T2
20.5 | card @{typ bool} = 2
20.6 | card T = Int.max (1, raw_card T)
20.7 - val neg_t = @{const Not} $ ObjectLogic.atomize_term thy t
20.8 + val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
20.9 val _ = fold_types (K o check_type ctxt) neg_t ()
20.10 val frees = Term.add_frees neg_t []
20.11 val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
21.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Mar 07 11:57:16 2010 +0100
21.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Mar 07 12:19:47 2010 +0100
21.3 @@ -1762,8 +1762,8 @@
21.4 (* theory -> styp -> term -> term list * term list * term *)
21.5 fun triple_for_intro_rule thy x t =
21.6 let
21.7 - val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
21.8 - val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
21.9 + val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
21.10 + val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
21.11 val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
21.12 (* term -> bool *)
21.13 val is_good_head = curry (op =) (Const x) o head_of
22.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Mar 07 11:57:16 2010 +0100
22.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Mar 07 12:19:47 2010 +0100
22.3 @@ -807,7 +807,7 @@
22.4 fun try_out negate =
22.5 let
22.6 val concl = (negate ? curry (op $) @{const Not})
22.7 - (ObjectLogic.atomize_term thy prop)
22.8 + (Object_Logic.atomize_term thy prop)
22.9 val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
22.10 |> map_types (map_type_tfree
22.11 (fn (s, []) => TFree (s, HOLogic.typeS)
23.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sun Mar 07 11:57:16 2010 +0100
23.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sun Mar 07 12:19:47 2010 +0100
23.3 @@ -225,9 +225,9 @@
23.4 (case dlo_instance ctxt p of
23.5 NONE => no_tac
23.6 | SOME instance =>
23.7 - ObjectLogic.full_atomize_tac i THEN
23.8 + Object_Logic.full_atomize_tac i THEN
23.9 simp_tac (#simpset (snd instance)) i THEN (* FIXME already part of raw_ferrack_qe_conv? *)
23.10 - CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
23.11 + CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
23.12 simp_tac (simpset_of ctxt) i)); (* FIXME really? *)
23.13
23.14 end;
24.1 --- a/src/HOL/Tools/Qelim/langford.ML Sun Mar 07 11:57:16 2010 +0100
24.2 +++ b/src/HOL/Tools/Qelim/langford.ML Sun Mar 07 12:19:47 2010 +0100
24.3 @@ -234,11 +234,11 @@
24.4 (case dlo_instance ctxt p of
24.5 (ss, NONE) => simp_tac ss i
24.6 | (ss, SOME instance) =>
24.7 - ObjectLogic.full_atomize_tac i THEN
24.8 + Object_Logic.full_atomize_tac i THEN
24.9 simp_tac ss i
24.10 THEN (CONVERSION Thm.eta_long_conversion) i
24.11 THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
24.12 - THEN ObjectLogic.full_atomize_tac i
24.13 - THEN CONVERSION (ObjectLogic.judgment_conv (raw_dlo_conv ss instance)) i
24.14 + THEN Object_Logic.full_atomize_tac i
24.15 + THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i
24.16 THEN (simp_tac ss i)));
24.17 end;
24.18 \ No newline at end of file
25.1 --- a/src/HOL/Tools/Qelim/presburger.ML Sun Mar 07 11:57:16 2010 +0100
25.2 +++ b/src/HOL/Tools/Qelim/presburger.ML Sun Mar 07 12:19:47 2010 +0100
25.3 @@ -166,13 +166,13 @@
25.4 val aprems = Arith_Data.get_arith_facts ctxt
25.5 in
25.6 Method.insert_tac aprems
25.7 - THEN_ALL_NEW ObjectLogic.full_atomize_tac
25.8 + THEN_ALL_NEW Object_Logic.full_atomize_tac
25.9 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
25.10 THEN_ALL_NEW simp_tac ss
25.11 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
25.12 - THEN_ALL_NEW ObjectLogic.full_atomize_tac
25.13 + THEN_ALL_NEW Object_Logic.full_atomize_tac
25.14 THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
25.15 - THEN_ALL_NEW ObjectLogic.full_atomize_tac
25.16 + THEN_ALL_NEW Object_Logic.full_atomize_tac
25.17 THEN_ALL_NEW div_mod_tac ctxt
25.18 THEN_ALL_NEW splits_tac ctxt
25.19 THEN_ALL_NEW simp_tac ss
26.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Mar 07 11:57:16 2010 +0100
26.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Mar 07 12:19:47 2010 +0100
26.3 @@ -48,7 +48,7 @@
26.4 fun atomize_thm thm =
26.5 let
26.6 val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
26.7 - val thm'' = ObjectLogic.atomize (cprop_of thm')
26.8 + val thm'' = Object_Logic.atomize (cprop_of thm')
26.9 in
26.10 @{thm equal_elim_rule1} OF [thm'', thm']
26.11 end
26.12 @@ -616,7 +616,7 @@
26.13
26.14 (* the tactic leaves three subgoals to be proved *)
26.15 fun procedure_tac ctxt rthm =
26.16 - ObjectLogic.full_atomize_tac
26.17 + Object_Logic.full_atomize_tac
26.18 THEN' gen_frees_tac ctxt
26.19 THEN' SUBGOAL (fn (goal, i) =>
26.20 let
27.1 --- a/src/HOL/Tools/TFL/post.ML Sun Mar 07 11:57:16 2010 +0100
27.2 +++ b/src/HOL/Tools/TFL/post.ML Sun Mar 07 12:19:47 2010 +0100
27.3 @@ -151,9 +151,9 @@
27.4 {f = f, R = R, rules = rules,
27.5 full_pats_TCs = full_pats_TCs,
27.6 TCs = TCs}
27.7 - val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm)
27.8 + val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
27.9 (R.CONJUNCTS rules)
27.10 - in {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
27.11 + in {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
27.12 rules = ListPair.zip(rules', rows),
27.13 tcs = (termination_goals rules') @ tcs}
27.14 end
27.15 @@ -180,7 +180,7 @@
27.16 | solve_eq (th, [a], i) = [(a, i)]
27.17 | solve_eq (th, splitths as (_ :: _), i) =
27.18 (writeln "Proving unsplit equation...";
27.19 - [((Drule.export_without_context o ObjectLogic.rulify_no_asm)
27.20 + [((Drule.export_without_context o Object_Logic.rulify_no_asm)
27.21 (CaseSplit.splitto splitths th), i)])
27.22 (* if there's an error, pretend nothing happened with this definition
27.23 We should probably print something out so that the user knows...? *)
28.1 --- a/src/HOL/Tools/choice_specification.ML Sun Mar 07 11:57:16 2010 +0100
28.2 +++ b/src/HOL/Tools/choice_specification.ML Sun Mar 07 12:19:47 2010 +0100
28.3 @@ -111,7 +111,7 @@
28.4 | myfoldr f [] = error "Choice_Specification.process_spec internal error"
28.5
28.6 val rew_imps = alt_props |>
28.7 - map (ObjectLogic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
28.8 + map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
28.9 val props' = rew_imps |>
28.10 map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
28.11
29.1 --- a/src/HOL/Tools/hologic.ML Sun Mar 07 11:57:16 2010 +0100
29.2 +++ b/src/HOL/Tools/hologic.ML Sun Mar 07 12:19:47 2010 +0100
29.3 @@ -190,14 +190,14 @@
29.4
29.5 fun conj_intr thP thQ =
29.6 let
29.7 - val (P, Q) = pairself (ObjectLogic.dest_judgment o Thm.cprop_of) (thP, thQ)
29.8 + val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
29.9 handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
29.10 val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
29.11 in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
29.12
29.13 fun conj_elim thPQ =
29.14 let
29.15 - val (P, Q) = Thm.dest_binop (ObjectLogic.dest_judgment (Thm.cprop_of thPQ))
29.16 + val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment (Thm.cprop_of thPQ))
29.17 handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
29.18 val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
29.19 val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
30.1 --- a/src/HOL/Tools/inductive.ML Sun Mar 07 11:57:16 2010 +0100
30.2 +++ b/src/HOL/Tools/inductive.ML Sun Mar 07 12:19:47 2010 +0100
30.3 @@ -788,7 +788,7 @@
30.4 else if coind then
30.5 singleton (ProofContext.export
30.6 (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
30.7 - (rotate_prems ~1 (ObjectLogic.rulify
30.8 + (rotate_prems ~1 (Object_Logic.rulify
30.9 (fold_rule rec_preds_defs
30.10 (rewrite_rule simp_thms'''
30.11 (mono RS (fp_def RS @{thm def_coinduct}))))))
31.1 --- a/src/HOL/Tools/inductive_realizer.ML Sun Mar 07 11:57:16 2010 +0100
31.2 +++ b/src/HOL/Tools/inductive_realizer.ML Sun Mar 07 12:19:47 2010 +0100
31.3 @@ -395,7 +395,7 @@
31.4 [rtac (#raw_induct ind_info) 1,
31.5 rewrite_goals_tac rews,
31.6 REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
31.7 - [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
31.8 + [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
31.9 DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
31.10 val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
31.11 (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
31.12 @@ -454,7 +454,7 @@
31.13 etac elimR 1,
31.14 ALLGOALS (asm_simp_tac HOL_basic_ss),
31.15 rewrite_goals_tac rews,
31.16 - REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
31.17 + REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
31.18 DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
31.19 val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
31.20 (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
32.1 --- a/src/HOL/Tools/lin_arith.ML Sun Mar 07 11:57:16 2010 +0100
32.2 +++ b/src/HOL/Tools/lin_arith.ML Sun Mar 07 12:19:47 2010 +0100
32.3 @@ -901,7 +901,7 @@
32.4 in
32.5
32.6 fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
32.7 - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
32.8 + Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
32.9
32.10 val tac = gen_tac true;
32.11
33.1 --- a/src/HOL/Tools/meson.ML Sun Mar 07 11:57:16 2010 +0100
33.2 +++ b/src/HOL/Tools/meson.ML Sun Mar 07 12:19:47 2010 +0100
33.3 @@ -587,7 +587,7 @@
33.4 Function mkcl converts theorems to clauses.*)
33.5 fun MESON mkcl cltac ctxt i st =
33.6 SELECT_GOAL
33.7 - (EVERY [ObjectLogic.atomize_prems_tac 1,
33.8 + (EVERY [Object_Logic.atomize_prems_tac 1,
33.9 rtac ccontr 1,
33.10 Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
33.11 EVERY1 [skolemize_prems_tac ctxt negs,
34.1 --- a/src/HOL/Tools/record.ML Sun Mar 07 11:57:16 2010 +0100
34.2 +++ b/src/HOL/Tools/record.ML Sun Mar 07 12:19:47 2010 +0100
34.3 @@ -2214,7 +2214,7 @@
34.4 [(cterm_of defs_thy Pvar, cterm_of defs_thy
34.5 (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
34.6 induct_scheme;
34.7 - in ObjectLogic.rulify (mp OF [ind, refl]) end;
34.8 + in Object_Logic.rulify (mp OF [ind, refl]) end;
34.9
34.10 val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
34.11 val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
35.1 --- a/src/HOL/Tools/res_axioms.ML Sun Mar 07 11:57:16 2010 +0100
35.2 +++ b/src/HOL/Tools/res_axioms.ML Sun Mar 07 12:19:47 2010 +0100
35.3 @@ -276,7 +276,7 @@
35.4 let val th1 = th |> transform_elim |> zero_var_indexes
35.5 val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
35.6 val th3 = th2
35.7 - |> Conv.fconv_rule ObjectLogic.atomize
35.8 + |> Conv.fconv_rule Object_Logic.atomize
35.9 |> Meson.make_nnf ctxt |> strip_lambdas ~1
35.10 in (th3, ctxt) end;
35.11
35.12 @@ -493,7 +493,7 @@
35.13 (*** Converting a subgoal into negated conjecture clauses. ***)
35.14
35.15 fun neg_skolemize_tac ctxt =
35.16 - EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt];
35.17 + EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
35.18
35.19 val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
35.20
36.1 --- a/src/HOL/Tools/sat_funcs.ML Sun Mar 07 11:57:16 2010 +0100
36.2 +++ b/src/HOL/Tools/sat_funcs.ML Sun Mar 07 12:19:47 2010 +0100
36.3 @@ -434,7 +434,7 @@
36.4
36.5 val pre_cnf_tac =
36.6 rtac ccontr THEN'
36.7 - ObjectLogic.atomize_prems_tac THEN'
36.8 + Object_Logic.atomize_prems_tac THEN'
36.9 CONVERSION Drule.beta_eta_conversion;
36.10
36.11 (* ------------------------------------------------------------------------- *)
37.1 --- a/src/HOL/Tools/typedef.ML Sun Mar 07 11:57:16 2010 +0100
37.2 +++ b/src/HOL/Tools/typedef.ML Sun Mar 07 12:19:47 2010 +0100
37.3 @@ -130,7 +130,7 @@
37.4 in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
37.5
37.6 fun typedef_result inhabited =
37.7 - ObjectLogic.typedecl (tname, vs, mx)
37.8 + Object_Logic.typedecl (tname, vs, mx)
37.9 #> snd
37.10 #> Sign.add_consts_i
37.11 [(Rep_name, newT --> oldT, NoSyn),
38.1 --- a/src/Provers/blast.ML Sun Mar 07 11:57:16 2010 +0100
38.2 +++ b/src/Provers/blast.ML Sun Mar 07 12:19:47 2010 +0100
38.3 @@ -181,7 +181,7 @@
38.4 fun isGoal (Const ("*Goal*", _) $ _) = true
38.5 | isGoal _ = false;
38.6
38.7 -val TruepropC = ObjectLogic.judgment_name Data.thy;
38.8 +val TruepropC = Object_Logic.judgment_name Data.thy;
38.9 val TruepropT = Sign.the_const_type Data.thy TruepropC;
38.10
38.11 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
38.12 @@ -1251,7 +1251,7 @@
38.13 fun timing_depth_tac start cs lim i st0 =
38.14 let val thy = Thm.theory_of_thm st0
38.15 val state = initialize thy
38.16 - val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0
38.17 + val st = Conv.gconv_rule Object_Logic.atomize_prems i st0
38.18 val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
38.19 val hyps = strip_imp_prems skoprem
38.20 and concl = strip_imp_concl skoprem
39.1 --- a/src/Provers/classical.ML Sun Mar 07 11:57:16 2010 +0100
39.2 +++ b/src/Provers/classical.ML Sun Mar 07 12:19:47 2010 +0100
39.3 @@ -153,7 +153,7 @@
39.4 *)
39.5
39.6 fun classical_rule rule =
39.7 - if ObjectLogic.is_elim rule then
39.8 + if Object_Logic.is_elim rule then
39.9 let
39.10 val rule' = rule RS classical;
39.11 val concl' = Thm.concl_of rule';
39.12 @@ -173,7 +173,7 @@
39.13 else rule;
39.14
39.15 (*flatten nested meta connectives in prems*)
39.16 -val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
39.17 +val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
39.18
39.19
39.20 (*** Useful tactics for classical reasoning ***)
39.21 @@ -724,24 +724,24 @@
39.22
39.23 (*Dumb but fast*)
39.24 fun fast_tac cs =
39.25 - ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
39.26 + Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
39.27
39.28 (*Slower but smarter than fast_tac*)
39.29 fun best_tac cs =
39.30 - ObjectLogic.atomize_prems_tac THEN'
39.31 + Object_Logic.atomize_prems_tac THEN'
39.32 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
39.33
39.34 (*even a bit smarter than best_tac*)
39.35 fun first_best_tac cs =
39.36 - ObjectLogic.atomize_prems_tac THEN'
39.37 + Object_Logic.atomize_prems_tac THEN'
39.38 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
39.39
39.40 fun slow_tac cs =
39.41 - ObjectLogic.atomize_prems_tac THEN'
39.42 + Object_Logic.atomize_prems_tac THEN'
39.43 SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
39.44
39.45 fun slow_best_tac cs =
39.46 - ObjectLogic.atomize_prems_tac THEN'
39.47 + Object_Logic.atomize_prems_tac THEN'
39.48 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
39.49
39.50
39.51 @@ -749,13 +749,13 @@
39.52 val weight_ASTAR = Unsynchronized.ref 5;
39.53
39.54 fun astar_tac cs =
39.55 - ObjectLogic.atomize_prems_tac THEN'
39.56 + Object_Logic.atomize_prems_tac THEN'
39.57 SELECT_GOAL
39.58 (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
39.59 (step_tac cs 1));
39.60
39.61 fun slow_astar_tac cs =
39.62 - ObjectLogic.atomize_prems_tac THEN'
39.63 + Object_Logic.atomize_prems_tac THEN'
39.64 SELECT_GOAL
39.65 (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
39.66 (slow_step_tac cs 1));
40.1 --- a/src/Provers/splitter.ML Sun Mar 07 11:57:16 2010 +0100
40.2 +++ b/src/Provers/splitter.ML Sun Mar 07 12:19:47 2010 +0100
40.3 @@ -46,14 +46,14 @@
40.4 struct
40.5
40.6 val Const (const_not, _) $ _ =
40.7 - ObjectLogic.drop_judgment Data.thy
40.8 + Object_Logic.drop_judgment Data.thy
40.9 (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
40.10
40.11 val Const (const_or , _) $ _ $ _ =
40.12 - ObjectLogic.drop_judgment Data.thy
40.13 + Object_Logic.drop_judgment Data.thy
40.14 (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
40.15
40.16 -val const_Trueprop = ObjectLogic.judgment_name Data.thy;
40.17 +val const_Trueprop = Object_Logic.judgment_name Data.thy;
40.18
40.19
40.20 fun split_format_err () = error "Wrong format for split rule";
41.1 --- a/src/Pure/Isar/attrib.ML Sun Mar 07 11:57:16 2010 +0100
41.2 +++ b/src/Pure/Isar/attrib.ML Sun Mar 07 12:19:47 2010 +0100
41.3 @@ -252,7 +252,7 @@
41.4 (* rule format *)
41.5
41.6 val rule_format = Args.mode "no_asm"
41.7 - >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format);
41.8 + >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
41.9
41.10 val elim_format = Thm.rule_attribute (K Tactic.make_elim);
41.11
41.12 @@ -306,9 +306,9 @@
41.13 setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
41.14 setup (Binding.name "eta_long") (Scan.succeed eta_long)
41.15 "put theorem into eta long beta normal form" #>
41.16 - setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize)
41.17 + setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
41.18 "declaration of atomize rule" #>
41.19 - setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
41.20 + setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
41.21 "declaration of rulify rule" #>
41.22 setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
41.23 setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
42.1 --- a/src/Pure/Isar/auto_bind.ML Sun Mar 07 11:57:16 2010 +0100
42.2 +++ b/src/Pure/Isar/auto_bind.ML Sun Mar 07 12:19:47 2010 +0100
42.3 @@ -23,7 +23,7 @@
42.4 val thisN = "this";
42.5 val assmsN = "assms";
42.6
42.7 -fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
42.8 +fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
42.9
42.10 fun statement_binds thy name prop =
42.11 [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
43.1 --- a/src/Pure/Isar/element.ML Sun Mar 07 11:57:16 2010 +0100
43.2 +++ b/src/Pure/Isar/element.ML Sun Mar 07 12:19:47 2010 +0100
43.3 @@ -223,12 +223,12 @@
43.4 val cert = Thm.cterm_of thy;
43.5
43.6 val th = MetaSimplifier.norm_hhf raw_th;
43.7 - val is_elim = ObjectLogic.is_elim th;
43.8 + val is_elim = Object_Logic.is_elim th;
43.9
43.10 val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
43.11 val prop = Thm.prop_of th';
43.12 val (prems, concl) = Logic.strip_horn prop;
43.13 - val concl_term = ObjectLogic.drop_judgment thy concl;
43.14 + val concl_term = Object_Logic.drop_judgment thy concl;
43.15
43.16 val fixes = fold_aterms (fn v as Free (x, T) =>
43.17 if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
44.1 --- a/src/Pure/Isar/expression.ML Sun Mar 07 11:57:16 2010 +0100
44.2 +++ b/src/Pure/Isar/expression.ML Sun Mar 07 12:19:47 2010 +0100
44.3 @@ -595,11 +595,11 @@
44.4 fun atomize_spec thy ts =
44.5 let
44.6 val t = Logic.mk_conjunction_balanced ts;
44.7 - val body = ObjectLogic.atomize_term thy t;
44.8 + val body = Object_Logic.atomize_term thy t;
44.9 val bodyT = Term.fastype_of body;
44.10 in
44.11 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
44.12 - else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
44.13 + else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
44.14 end;
44.15
44.16 (* achieve plain syntax for locale predicates (without "PROP") *)
44.17 @@ -634,7 +634,7 @@
44.18
44.19 val args = map Logic.mk_type extraTs @ map Free xs;
44.20 val head = Term.list_comb (Const (name, predT), args);
44.21 - val statement = ObjectLogic.ensure_propT thy head;
44.22 + val statement = Object_Logic.ensure_propT thy head;
44.23
44.24 val ([pred_def], defs_thy) =
44.25 thy
45.1 --- a/src/Pure/Isar/isar_syn.ML Sun Mar 07 11:57:16 2010 +0100
45.2 +++ b/src/Pure/Isar/isar_syn.ML Sun Mar 07 12:19:47 2010 +0100
45.3 @@ -105,7 +105,7 @@
45.4 val _ =
45.5 OuterSyntax.command "typedecl" "type declaration" K.thy_decl
45.6 (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
45.7 - Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
45.8 + Toplevel.theory (Object_Logic.typedecl (a, args, mx) #> snd)));
45.9
45.10 val _ =
45.11 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
45.12 @@ -127,7 +127,7 @@
45.13
45.14 val _ =
45.15 OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
45.16 - (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd));
45.17 + (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
45.18
45.19 val _ =
45.20 OuterSyntax.command "consts" "declare constants" K.thy_decl
46.1 --- a/src/Pure/Isar/method.ML Sun Mar 07 11:57:16 2010 +0100
46.2 +++ b/src/Pure/Isar/method.ML Sun Mar 07 12:19:47 2010 +0100
46.3 @@ -171,8 +171,8 @@
46.4
46.5 (* atomize rule statements *)
46.6
46.7 -fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
46.8 - | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
46.9 +fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
46.10 + | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
46.11
46.12
46.13 (* this -- resolve facts directly *)
47.1 --- a/src/Pure/Isar/object_logic.ML Sun Mar 07 11:57:16 2010 +0100
47.2 +++ b/src/Pure/Isar/object_logic.ML Sun Mar 07 12:19:47 2010 +0100
47.3 @@ -34,7 +34,7 @@
47.4 val rule_format_no_asm: attribute
47.5 end;
47.6
47.7 -structure ObjectLogic: OBJECT_LOGIC =
47.8 +structure Object_Logic: OBJECT_LOGIC =
47.9 struct
47.10
47.11 (** theory data **)
48.1 --- a/src/Pure/Isar/obtain.ML Sun Mar 07 11:57:16 2010 +0100
48.2 +++ b/src/Pure/Isar/obtain.ML Sun Mar 07 12:19:47 2010 +0100
48.3 @@ -76,7 +76,7 @@
48.4 val thy = ProofContext.theory_of fix_ctxt;
48.5
48.6 val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
48.7 - val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
48.8 + val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
48.9 error "Conclusion in obtained context must be object-logic judgment";
48.10
48.11 val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
48.12 @@ -100,7 +100,7 @@
48.13 fun bind_judgment ctxt name =
48.14 let
48.15 val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
48.16 - val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
48.17 + val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) name);
48.18 in ((v, t), ctxt') end;
48.19
48.20 val thatN = "that";
49.1 --- a/src/Pure/Isar/rule_cases.ML Sun Mar 07 11:57:16 2010 +0100
49.2 +++ b/src/Pure/Isar/rule_cases.ML Sun Mar 07 12:19:47 2010 +0100
49.3 @@ -110,7 +110,7 @@
49.4 val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
49.5 |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
49.6
49.7 - val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
49.8 + val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
49.9 val binds =
49.10 (case_conclN, concl) :: dest_binops concls concl
49.11 |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
50.1 --- a/src/Pure/Isar/specification.ML Sun Mar 07 11:57:16 2010 +0100
50.2 +++ b/src/Pure/Isar/specification.ML Sun Mar 07 12:19:47 2010 +0100
50.3 @@ -316,7 +316,7 @@
50.4 val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
50.5 val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
50.6
50.7 - val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
50.8 + val thesis = Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
50.9
50.10 fun assume_case ((name, (vars, _)), asms) ctxt' =
50.11 let
51.1 --- a/src/Pure/Thy/term_style.ML Sun Mar 07 11:57:16 2010 +0100
51.2 +++ b/src/Pure/Thy/term_style.ML Sun Mar 07 12:19:47 2010 +0100
51.3 @@ -64,8 +64,8 @@
51.4
51.5 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
51.6 let
51.7 - val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
51.8 - (Logic.strip_imp_concl t)
51.9 + val concl =
51.10 + Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
51.11 in
51.12 case concl of (_ $ l $ r) => proj (l, r)
51.13 | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
52.1 --- a/src/Pure/Tools/find_theorems.ML Sun Mar 07 11:57:16 2010 +0100
52.2 +++ b/src/Pure/Tools/find_theorems.ML Sun Mar 07 12:19:47 2010 +0100
52.3 @@ -93,7 +93,7 @@
52.4
52.5 (* matching theorems *)
52.6
52.7 -fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
52.8 +fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
52.9
52.10 (*educated guesses on HOL*) (* FIXME broken *)
52.11 val boolT = Type ("bool", []);
52.12 @@ -110,13 +110,13 @@
52.13 fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
52.14 fun matches pat =
52.15 let
52.16 - val jpat = ObjectLogic.drop_judgment thy pat;
52.17 + val jpat = Object_Logic.drop_judgment thy pat;
52.18 val c = Term.head_of jpat;
52.19 val pats =
52.20 if Term.is_Const c
52.21 then
52.22 if doiff andalso c = iff_const then
52.23 - (pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat)))
52.24 + (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
52.25 |> filter (is_nontrivial thy)
52.26 else [pat]
52.27 else [];
53.1 --- a/src/Pure/old_goals.ML Sun Mar 07 11:57:16 2010 +0100
53.2 +++ b/src/Pure/old_goals.ML Sun Mar 07 12:19:47 2010 +0100
53.3 @@ -606,11 +606,11 @@
53.4 fun qed_goalw name thy rews goal tacsf =
53.5 ML_Context.ml_store_thm (name, prove_goalw thy rews goal tacsf);
53.6 fun qed_spec_mp name =
53.7 - ML_Context.ml_store_thm (name, ObjectLogic.rulify_no_asm (result ()));
53.8 + ML_Context.ml_store_thm (name, Object_Logic.rulify_no_asm (result ()));
53.9 fun qed_goal_spec_mp name thy s p =
53.10 - bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p));
53.11 + bind_thm (name, Object_Logic.rulify_no_asm (prove_goal thy s p));
53.12 fun qed_goalw_spec_mp name thy defs s p =
53.13 - bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
53.14 + bind_thm (name, Object_Logic.rulify_no_asm (prove_goalw thy defs s p));
53.15
53.16 end;
53.17
54.1 --- a/src/Tools/atomize_elim.ML Sun Mar 07 11:57:16 2010 +0100
54.2 +++ b/src/Tools/atomize_elim.ML Sun Mar 07 12:19:47 2010 +0100
54.3 @@ -59,9 +59,9 @@
54.4 (EX x y z. ...) | ... | (EX a b c. ...)
54.5 *)
54.6 fun atomize_elim_conv ctxt ct =
54.7 - (forall_conv (K (prems_conv ~1 ObjectLogic.atomize_prems)) ctxt
54.8 + (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
54.9 then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
54.10 - then_conv (fn ct' => if can ObjectLogic.dest_judgment ct'
54.11 + then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
54.12 then all_conv ct'
54.13 else raise CTERM ("atomize_elim", [ct', ct])))
54.14 ct
55.1 --- a/src/Tools/induct.ML Sun Mar 07 11:57:16 2010 +0100
55.2 +++ b/src/Tools/induct.ML Sun Mar 07 12:19:47 2010 +0100
55.3 @@ -137,7 +137,7 @@
55.4 Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
55.5 Conv.rewr_conv Drule.swap_prems_eq
55.6
55.7 -fun drop_judgment ctxt = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt);
55.8 +fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
55.9
55.10 fun find_eq ctxt t =
55.11 let
55.12 @@ -511,7 +511,7 @@
55.13
55.14 fun atomize_term thy =
55.15 MetaSimplifier.rewrite_term thy Data.atomize []
55.16 - #> ObjectLogic.drop_judgment thy;
55.17 + #> Object_Logic.drop_judgment thy;
55.18
55.19 val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
55.20
56.1 --- a/src/Tools/induct_tacs.ML Sun Mar 07 11:57:16 2010 +0100
56.2 +++ b/src/Tools/induct_tacs.ML Sun Mar 07 12:19:47 2010 +0100
56.3 @@ -92,7 +92,7 @@
56.4 (_, rule) :: _ => rule
56.5 | [] => raise THM ("No induction rules", 0, [])));
56.6
56.7 - val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
56.8 + val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
56.9 val _ = Method.trace ctxt [rule'];
56.10
56.11 val concls = Logic.dest_conjunctions (Thm.concl_of rule);
57.1 --- a/src/Tools/intuitionistic.ML Sun Mar 07 11:57:16 2010 +0100
57.2 +++ b/src/Tools/intuitionistic.ML Sun Mar 07 12:19:47 2010 +0100
57.3 @@ -89,7 +89,7 @@
57.4 Method.setup name
57.5 (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
57.6 (fn opt_lim => fn ctxt =>
57.7 - SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
57.8 + SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
57.9 "intuitionistic proof search";
57.10
57.11 end;
58.1 --- a/src/Tools/quickcheck.ML Sun Mar 07 11:57:16 2010 +0100
58.2 +++ b/src/Tools/quickcheck.ML Sun Mar 07 12:19:47 2010 +0100
58.3 @@ -199,7 +199,7 @@
58.4 val gi' = Logic.list_implies (if no_assms then [] else assms,
58.5 subst_bounds (frees, strip gi))
58.6 |> monomorphic_term thy insts default_T
58.7 - |> ObjectLogic.atomize_term thy;
58.8 + |> Object_Logic.atomize_term thy;
58.9 in gen_test_term ctxt quiet report generator_name size iterations gi' end;
58.10
58.11 fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."