--- a/src/HOL/Calculation.thy Mon Jul 31 14:37:18 2000 +0200
+++ b/src/HOL/Calculation.thy Tue Aug 01 00:18:40 2000 +0200
@@ -8,40 +8,40 @@
theory Calculation = IntArith:
-theorem forw_subst: "a = b ==> P b ==> P a"
+lemma forw_subst: "a = b ==> P b ==> P a"
by (rule ssubst)
-theorem back_subst: "P a ==> a = b ==> P b"
+lemma back_subst: "P a ==> a = b ==> P b"
by (rule subst)
-theorem set_rev_mp: "x:A ==> A <= B ==> x:B"
+lemma set_rev_mp: "x:A ==> A <= B ==> x:B"
by (rule subsetD)
-theorem set_mp: "A <= B ==> x:A ==> x:B"
+lemma set_mp: "A <= B ==> x:A ==> x:B"
by (rule subsetD)
-theorem order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
+lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
by (simp add: order_less_le)
-theorem order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
+lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
by (simp add: order_less_le)
-theorem order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
+lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
by (rule order_less_asym)
-theorem ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
+lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
by (rule subst)
-theorem ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
+lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
by (rule ssubst)
-theorem ord_less_eq_trans: "a < b ==> b = c ==> a < c"
+lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
by (rule subst)
-theorem ord_eq_less_trans: "a = b ==> b < c ==> a < c"
+lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
by (rule ssubst)
-theorem order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
+lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
(!!x y. x < y ==> f x < f y) ==> f a < c"
proof -
assume r: "!!x y. x < y ==> f x < f y"
@@ -50,7 +50,7 @@
finally (order_less_trans) show ?thesis .
qed
-theorem order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
+lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
(!!x y. x < y ==> f x < f y) ==> a < f c"
proof -
assume r: "!!x y. x < y ==> f x < f y"
@@ -59,7 +59,7 @@
finally (order_less_trans) show ?thesis .
qed
-theorem order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
+lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
(!!x y. x <= y ==> f x <= f y) ==> f a < c"
proof -
assume r: "!!x y. x <= y ==> f x <= f y"
@@ -68,7 +68,7 @@
finally (order_le_less_trans) show ?thesis .
qed
-theorem order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
+lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
(!!x y. x < y ==> f x < f y) ==> a < f c"
proof -
assume r: "!!x y. x < y ==> f x < f y"
@@ -77,7 +77,7 @@
finally (order_le_less_trans) show ?thesis .
qed
-theorem order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
+lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
(!!x y. x < y ==> f x < f y) ==> f a < c"
proof -
assume r: "!!x y. x < y ==> f x < f y"
@@ -86,7 +86,7 @@
finally (order_less_le_trans) show ?thesis .
qed
-theorem order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
+lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
(!!x y. x <= y ==> f x <= f y) ==> a < f c"
proof -
assume r: "!!x y. x <= y ==> f x <= f y"
@@ -95,7 +95,7 @@
finally (order_less_le_trans) show ?thesis .
qed
-theorem order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
+lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
(!!x y. x <= y ==> f x <= f y) ==> a <= f c"
proof -
assume r: "!!x y. x <= y ==> f x <= f y"
@@ -104,7 +104,7 @@
finally (order_trans) show ?thesis .
qed
-theorem order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
+lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
(!!x y. x <= y ==> f x <= f y) ==> f a <= c"
proof -
assume r: "!!x y. x <= y ==> f x <= f y"
@@ -113,7 +113,7 @@
finally (order_trans) show ?thesis .
qed
-theorem ord_le_eq_subst: "a <= b ==> f b = c ==>
+lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
(!!x y. x <= y ==> f x <= f y) ==> f a <= c"
proof -
assume r: "!!x y. x <= y ==> f x <= f y"
@@ -122,7 +122,7 @@
finally (ord_le_eq_trans) show ?thesis .
qed
-theorem ord_eq_le_subst: "a = f b ==> b <= c ==>
+lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
(!!x y. x <= y ==> f x <= f y) ==> a <= f c"
proof -
assume r: "!!x y. x <= y ==> f x <= f y"
@@ -131,7 +131,7 @@
finally (ord_eq_le_trans) show ?thesis .
qed
-theorem ord_less_eq_subst: "a < b ==> f b = c ==>
+lemma ord_less_eq_subst: "a < b ==> f b = c ==>
(!!x y. x < y ==> f x < f y) ==> f a < c"
proof -
assume r: "!!x y. x < y ==> f x < f y"
@@ -140,7 +140,7 @@
finally (ord_less_eq_trans) show ?thesis .
qed
-theorem ord_eq_less_subst: "a = f b ==> b < c ==>
+lemma ord_eq_less_subst: "a = f b ==> b < c ==>
(!!x y. x < y ==> f x < f y) ==> a < f c"
proof -
assume r: "!!x y. x < y ==> f x < f y"
@@ -153,7 +153,7 @@
Note that this list of rules is in reverse order of priorities.
*}
-theorems trans_rules [trans] =
+lemmas trans_rules [trans] =
order_less_subst2
order_less_subst1
order_le_less_subst2
@@ -187,6 +187,6 @@
ord_eq_less_trans
trans
-theorems [elim?] = sym
+lemmas [elim?] = sym
end
--- a/src/Pure/Isar/proof.ML Mon Jul 31 14:37:18 2000 +0200
+++ b/src/Pure/Isar/proof.ML Tue Aug 01 00:18:40 2000 +0200
@@ -528,7 +528,6 @@
val hard_asm_tac = Tactic.etac Drule.triv_goal;
val soft_asm_tac = Tactic.rtac Drule.triv_goal;
- (* THEN' Tactic.rtac asm_rl FIXME hack to norm goal *)
val assm = gen_assume ProofContext.assume;
val assm_i = gen_assume ProofContext.assume_i;