33 val add_intro: thm -> theory -> theory |
33 val add_intro: thm -> theory -> theory |
34 val set_elim: thm -> theory -> theory |
34 val set_elim: thm -> theory -> theory |
35 val set_nparams : string -> int -> theory -> theory |
35 val set_nparams : string -> int -> theory -> theory |
36 val print_stored_rules: theory -> unit |
36 val print_stored_rules: theory -> unit |
37 val print_all_modes: theory -> unit |
37 val print_all_modes: theory -> unit |
38 val do_proofs: bool ref |
38 val do_proofs: bool Unsynchronized.ref |
39 val mk_casesrule : Proof.context -> int -> thm list -> term |
39 val mk_casesrule : Proof.context -> int -> thm list -> term |
40 val analyze_compr: theory -> term -> term |
40 val analyze_compr: theory -> term -> term |
41 val eval_ref: (unit -> term Predicate.pred) option ref |
41 val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref |
42 val add_equations : string list -> theory -> theory |
42 val add_equations : string list -> theory -> theory |
43 val code_pred_intros_attrib : attribute |
43 val code_pred_intros_attrib : attribute |
44 (* used by Quickcheck_Generator *) |
44 (* used by Quickcheck_Generator *) |
45 (*val funT_of : mode -> typ -> typ |
45 (*val funT_of : mode -> typ -> typ |
46 val mk_if_pred : term -> term |
46 val mk_if_pred : term -> term |
121 fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); |
121 fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); |
122 |
122 |
123 fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *) |
123 fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *) |
124 fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) |
124 fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) |
125 |
125 |
126 val do_proofs = ref true; |
126 val do_proofs = Unsynchronized.ref true; |
127 |
127 |
128 (* reference to preprocessing of InductiveSet package *) |
128 (* reference to preprocessing of InductiveSet package *) |
129 |
129 |
130 val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*) |
130 val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*) |
131 |
131 |
2332 val code_pred = generic_code_pred (K I); |
2332 val code_pred = generic_code_pred (K I); |
2333 val code_pred_cmd = generic_code_pred Code.read_const |
2333 val code_pred_cmd = generic_code_pred Code.read_const |
2334 |
2334 |
2335 (* transformation for code generation *) |
2335 (* transformation for code generation *) |
2336 |
2336 |
2337 val eval_ref = ref (NONE : (unit -> term Predicate.pred) option); |
2337 val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option); |
2338 |
2338 |
2339 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) |
2339 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) |
2340 fun analyze_compr thy t_compr = |
2340 fun analyze_compr thy t_compr = |
2341 let |
2341 let |
2342 val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t |
2342 val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t |