--- a/src/Pure/drule.ML Thu Mar 02 12:07:20 1995 +0100
+++ b/src/Pure/drule.ML Fri Mar 03 11:48:05 1995 +0100
@@ -421,9 +421,7 @@
(show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts);
in
(show_no_free_types := true; show_sorts := false;
-
Pretty.writeln (pretty_term B);
-
if ngoals = 0 then writeln "No subgoals!"
else if ngoals > maxgoals then
(print_goals (1, take (maxgoals, As));
@@ -640,22 +638,22 @@
val reflexive_thm =
- let val cx = cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),logicS)))
+ let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
in Thm.reflexive cx end;
val symmetric_thm =
- let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT)
+ let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
val transitive_thm =
- let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT)
- val yz = read_cterm Sign.pure ("y::'a::logic == z",propT)
+ let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
+ val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
val xythm = Thm.assume xy and yzthm = Thm.assume yz
in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
(** Below, a "conversion" has type cterm -> thm **)
-val refl_cimplies = reflexive (cterm_of Sign.pure implies);
+val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies);
(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
(*Do not rewrite flex-flex pairs*)
@@ -734,17 +732,17 @@
(*** Some useful meta-theorems ***)
(*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = trivial(read_cterm Sign.pure ("PROP ?psi",propT));
+val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
-val cut_rl = trivial(read_cterm Sign.pure
+val cut_rl = trivial(read_cterm Sign.proto_pure
("PROP ?psi ==> PROP ?theta", propT));
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
[| PROP V; PROP V ==> PROP W |] ==> PROP W *)
val revcut_rl =
- let val V = read_cterm Sign.pure ("PROP V", propT)
- and VW = read_cterm Sign.pure ("PROP V ==> PROP W", propT);
+ let val V = read_cterm Sign.proto_pure ("PROP V", propT)
+ and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
in standard (implies_intr V
(implies_intr VW
(implies_elim (assume VW) (assume V))))
@@ -752,16 +750,16 @@
(*for deleting an unwanted assumption*)
val thin_rl =
- let val V = read_cterm Sign.pure ("PROP V", propT)
- and W = read_cterm Sign.pure ("PROP W", propT);
+ let val V = read_cterm Sign.proto_pure ("PROP V", propT)
+ and W = read_cterm Sign.proto_pure ("PROP W", propT);
in standard (implies_intr V (implies_intr W (assume W)))
end;
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*)
val triv_forall_equality =
- let val V = read_cterm Sign.pure ("PROP V", propT)
- and QV = read_cterm Sign.pure ("!!x::'a. PROP V", propT)
- and x = read_cterm Sign.pure ("x", TFree("'a",logicS));
+ let val V = read_cterm Sign.proto_pure ("PROP V", propT)
+ and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
+ and x = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
in standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
(implies_intr V (forall_intr x (assume V))))
end;