# HG changeset patch
# User wenzelm
# Date 965081920 -7200
# Node ID 9c438a65be0a3406757a16e9d71e063c858bf08a
# Parent  b16624f1ea385d2cf7d4da2be775964fd4f6882a
tuned;

diff -r b16624f1ea38 -r 9c438a65be0a src/HOL/Calculation.thy
--- 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
diff -r b16624f1ea38 -r 9c438a65be0a src/Pure/Isar/proof.ML
--- 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;