--- a/src/HOL/Algebra/ringsimp.ML Thu Nov 23 22:38:28 2006 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Thu Nov 23 22:38:29 2006 +0100
@@ -1,13 +1,13 @@
(*
- Title: Normalisation method for locales ring and cring
Id: $Id$
Author: Clemens Ballarin
- Copyright: TU Muenchen
+
+Normalisation method for locales ring and cring.
*)
signature ALGEBRA =
sig
- val print_structures: Context.generic -> unit
+ val print_structures: Proof.context -> unit
val setup: theory -> theory
end;
@@ -44,7 +44,7 @@
end
end);
-val print_structures = AlgebraData.print;
+val print_structures = AlgebraData.print o Context.Proof;
(** Method **)
@@ -58,8 +58,7 @@
in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
fun algebra_tac ctxt =
- let val _ = print_structures (Context.Proof ctxt)
- in EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt))) end;
+ EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
val method =
Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt))
@@ -69,7 +68,7 @@
fun add_struct_thm s =
Thm.declaration_attribute (fn thm => fn ctxt =>
- AlgebraData.map (fn structs =>
+ AlgebraData.map (fn structs =>
if AList.defined struct_eq structs s
then AList.map_entry struct_eq s (fn thms => thm :: thms) structs
else (s, [thm])::structs) ctxt);
@@ -79,7 +78,7 @@
val attribute = Attrib.syntax
(Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
- Scan.succeed true) -- Scan.lift Args.name --
+ Scan.succeed true) -- Scan.lift Args.name --
Scan.repeat Args.term
>> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
@@ -92,4 +91,4 @@
Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
-end; (* struct *)
+end;
--- a/src/HOL/Tools/recdef_package.ML Thu Nov 23 22:38:28 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML Thu Nov 23 22:38:29 2006 +0100
@@ -11,7 +11,7 @@
val print_recdefs: theory -> unit
val get_recdef: theory -> string
-> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
- val get_hints: Context.generic -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
+ val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
val simp_add: attribute
val simp_del: attribute
val cong_add: attribute
@@ -130,7 +130,6 @@
in GlobalRecdefData.put (tab', hints) thy end;
val get_global_hints = #2 o GlobalRecdefData.get;
-val map_global_hints = GlobalRecdefData.map o apsnd;
(* proof data *)
@@ -143,17 +142,8 @@
fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
end);
-val get_local_hints = LocalRecdefData.get;
-val map_local_hints = LocalRecdefData.map;
-
-
-(* generic data *)
-
-fun get_hints (Context.Theory thy) = get_global_hints thy
- | get_hints (Context.Proof ctxt) = get_local_hints ctxt;
-
-fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
- | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
+val get_hints = LocalRecdefData.get;
+fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f);
(* attributes *)
@@ -197,7 +187,7 @@
(case opt_src of
NONE => ctxt0
| SOME src => Method.only_sectioned_args recdef_modifiers I src ctxt0);
- val {simps, congs, wfs} = get_local_hints ctxt;
+ val {simps, congs, wfs} = get_hints ctxt;
val cs = local_claset_of ctxt;
val ss = local_simpset_of ctxt addsimps simps;
in (cs, ss, rev (map snd congs), wfs) end;
--- a/src/HOL/Tools/res_axioms.ML Thu Nov 23 22:38:28 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Nov 23 22:38:29 2006 +0100
@@ -5,29 +5,25 @@
Transformation of axiom rules (elim/intro/etc) into CNF forms.
*)
-(*unused during debugging*)
signature RES_AXIOMS =
- sig
- val cnf_axiom : (string * thm) -> thm list
+sig
+ val trace_abs: bool ref
+ val cnf_axiom : string * thm -> thm list
val cnf_name : string -> thm list
val meta_cnf_axiom : thm -> thm list
- val claset_rules_of_thy : theory -> (string * thm) list
- val simpset_rules_of_thy : theory -> (string * thm) list
- val claset_rules_of_ctxt: Proof.context -> (string * thm) list
- val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
- val pairname : thm -> (string * thm)
+ val pairname : thm -> string * thm
val skolem_thm : thm -> thm list
val to_nnf : thm -> thm
- val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
+ val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
val meson_method_setup : theory -> theory
val setup : theory -> theory
+ val assume_abstract_list: thm list -> thm list
+ val claset_rules_of: Proof.context -> (string * thm) list
+ val simpset_rules_of: Proof.context -> (string * thm) list
+ val atpset_rules_of: Proof.context -> (string * thm) list
+end;
- val atpset_rules_of_thy : theory -> (string * thm) list
- val atpset_rules_of_ctxt : Proof.context -> (string * thm) list
- end;
-
-structure ResAxioms =
-
+structure ResAxioms: RES_AXIOMS =
struct
(*For running the comparison between combinators and abstractions.
@@ -552,16 +548,10 @@
map (fn r => (#name r, #thm r)) simps
end;
-fun claset_rules_of_thy thy = rules_of_claset (claset_of thy);
-fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy);
-
-fun atpset_rules_of_thy thy = map pairname (ResAtpset.get_atpset (Context.Theory thy));
+fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
+fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
-
-fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt);
-fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt);
-
-fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpset.get_atpset (Context.Proof ctxt));
+fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt);
(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)