Updated import configuration.
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Apr 01 18:59:17 2005 +0200
@@ -3,13 +3,13 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory GenHOL4Base = HOL4Compat + HOL4Syntax:;
+theory GenHOL4Base = "../HOL4Compat" + "../HOL4Syntax":;
import_segment "hol4";
setup_dump "../HOL" "HOL4Base";
-append_dump "theory HOL4Base = HOL4Compat + HOL4Syntax:";
+append_dump {*theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":*};
import_theory bool;
@@ -50,8 +50,8 @@
sum > "+";
const_maps
- INL > Inl
- INR > Inr
+ INL > Sum_Type.Inl
+ INR > Sum_Type.Inr
ISL > HOL4Compat.ISL
ISR > HOL4Compat.ISR
OUTL > HOL4Compat.OUTL
@@ -166,7 +166,7 @@
import_theory prim_rec;
const_maps
- "<" > "op <" :: "[nat,nat]\<Rightarrow>bool";
+ "<" > "op <" :: "[nat,nat]=>bool";
end_import;
@@ -181,15 +181,15 @@
">" > HOL4Compat.nat_gt
">=" > HOL4Compat.nat_ge
FUNPOW > HOL4Compat.FUNPOW
- "<=" > "op <=" :: "[nat,nat]\<Rightarrow>bool"
- "+" > "op +" :: "[nat,nat]\<Rightarrow>nat"
- "*" > "op *" :: "[nat,nat]\<Rightarrow>nat"
- "-" > "op -" :: "[nat,nat]\<Rightarrow>nat"
- MIN > HOL.min :: "[nat,nat]\<Rightarrow>nat"
- MAX > HOL.max :: "[nat,nat]\<Rightarrow>nat"
- DIV > "Divides.op div" :: "[nat,nat]\<Rightarrow>nat"
- MOD > "Divides.op mod" :: "[nat,nat]\<Rightarrow>nat"
- EXP > Nat.power :: "[nat,nat]\<Rightarrow>nat";
+ "<=" > "op <=" :: "[nat,nat]=>bool"
+ "+" > "op +" :: "[nat,nat]=>nat"
+ "*" > "op *" :: "[nat,nat]=>nat"
+ "-" > "op -" :: "[nat,nat]=>nat"
+ MIN > Orderings.min :: "[nat,nat]=>nat"
+ MAX > Orderings.max :: "[nat,nat]=>nat"
+ DIV > "Divides.op div" :: "[nat,nat]=>nat"
+ MOD > "Divides.op mod" :: "[nat,nat]=>nat"
+ EXP > Nat.power :: "[nat,nat]=>nat";
end_import;
@@ -208,7 +208,7 @@
import_theory divides;
const_maps
- divides > "Divides.op dvd" :: "[nat,nat]\<Rightarrow>bool";
+ divides > "Divides.op dvd" :: "[nat,nat]=>bool";
end_import;
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Apr 01 18:59:17 2005 +0200
@@ -19,11 +19,11 @@
const_maps
real_0 > 0 :: real
real_1 > 1 :: real
- real_neg > uminus :: "real \<Rightarrow> real"
- inv > HOL.inverse :: "real \<Rightarrow> real"
- real_add > "op +" :: "[real,real] \<Rightarrow> real"
- real_mul > "op *" :: "[real,real] \<Rightarrow> real"
- real_lt > "op <" :: "[real,real] \<Rightarrow> bool";
+ real_neg > uminus :: "real => real"
+ inv > HOL.inverse :: "real => real"
+ real_add > "op +" :: "[real,real] => real"
+ real_mul > "op *" :: "[real,real] => real"
+ real_lt > "op <" :: "[real,real] => bool";
ignore_thms
real_TY_DEF
@@ -51,12 +51,12 @@
const_maps
real_gt > HOL4Compat.real_gt
real_ge > HOL4Compat.real_ge
- real_lte > "op <=" :: "[real,real] \<Rightarrow> bool"
- real_sub > "op -" :: "[real,real] \<Rightarrow> real"
- "/" > HOL.divide :: "[real,real] \<Rightarrow> real"
- pow > Nat.power :: "[real,nat] \<Rightarrow> real"
- abs > HOL.abs :: "real \<Rightarrow> real"
- real_of_num > RealDef.real :: "nat \<Rightarrow> real";
+ real_lte > "op <=" :: "[real,real] => bool"
+ real_sub > "op -" :: "[real,real] => real"
+ "/" > HOL.divide :: "[real,real] => real"
+ pow > Nat.power :: "[real,nat] => real"
+ abs > HOL.abs :: "real => real"
+ real_of_num > RealDef.real :: "nat => real";
end_import;
--- a/src/HOL/Import/Generate-HOL/ROOT.ML Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/ROOT.ML Fri Apr 01 18:59:17 2005 +0200
@@ -3,8 +3,6 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-with_path ".." use_thy "HOL4Compat";
-with_path ".." use_thy "HOL4Syntax";
use_thy "GenHOL4Prob";
use_thy "GenHOL4Vec";
use_thy "GenHOL4Word32";
--- a/src/HOL/Import/HOL/HOL4Base.thy Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy Fri Apr 01 18:59:17 2005 +0200
@@ -1,4 +1,6 @@
-theory HOL4Base = HOL4Compat + HOL4Syntax:
+(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
+
+theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":
;setup_theory bool
@@ -755,7 +757,11 @@
lemma CURRY_ONE_ONE_THM: "(curry f = curry g) = (f = g)"
by (import pair CURRY_ONE_ONE_THM)
-lemma UNCURRY_ONE_ONE_THM: "(split f = split g) = (f = g)"
+lemma UNCURRY_ONE_ONE_THM: "(op =::bool => bool => bool)
+ ((op =::('a * 'b => 'c) => ('a * 'b => 'c) => bool)
+ ((split::('a => 'b => 'c) => 'a * 'b => 'c) (f::'a => 'b => 'c))
+ ((split::('a => 'b => 'c) => 'a * 'b => 'c) (g::'a => 'b => 'c)))
+ ((op =::('a => 'b => 'c) => ('a => 'b => 'c) => bool) f g)"
by (import pair UNCURRY_ONE_ONE_THM)
lemma pair_Axiom: "ALL f. EX x. ALL xa y. x (xa, y) = f xa y"
@@ -772,18 +778,53 @@
lemma ELIM_PFORALL: "(ALL p. P (fst p) (snd p)) = (ALL p1. All (P p1))"
by (import pair ELIM_PFORALL)
-lemma PFORALL_THM: "ALL x. (ALL xa. All (x xa)) = All (split x)"
+lemma PFORALL_THM: "(All::(('a => 'b => bool) => bool) => bool)
+ (%x::'a => 'b => bool.
+ (op =::bool => bool => bool)
+ ((All::('a => bool) => bool)
+ (%xa::'a. (All::('b => bool) => bool) (x xa)))
+ ((All::('a * 'b => bool) => bool)
+ ((split::('a => 'b => bool) => 'a * 'b => bool) x)))"
by (import pair PFORALL_THM)
-lemma PEXISTS_THM: "ALL x. (EX xa. Ex (x xa)) = Ex (split x)"
+lemma PEXISTS_THM: "(All::(('a => 'b => bool) => bool) => bool)
+ (%x::'a => 'b => bool.
+ (op =::bool => bool => bool)
+ ((Ex::('a => bool) => bool)
+ (%xa::'a. (Ex::('b => bool) => bool) (x xa)))
+ ((Ex::('a * 'b => bool) => bool)
+ ((split::('a => 'b => bool) => 'a * 'b => bool) x)))"
by (import pair PEXISTS_THM)
-lemma LET2_RAND: "ALL (x::'c => 'd) (xa::'a * 'b) xb::'a => 'b => 'c.
- x (Let xa (split xb)) = (let (xa::'a, y::'b) = xa in x (xb xa y))"
+lemma LET2_RAND: "(All::(('c => 'd) => bool) => bool)
+ (%x::'c => 'd.
+ (All::('a * 'b => bool) => bool)
+ (%xa::'a * 'b.
+ (All::(('a => 'b => 'c) => bool) => bool)
+ (%xb::'a => 'b => 'c.
+ (op =::'d => 'd => bool)
+ (x ((Let::'a * 'b => ('a * 'b => 'c) => 'c) xa
+ ((split::('a => 'b => 'c) => 'a * 'b => 'c) xb)))
+ ((Let::'a * 'b => ('a * 'b => 'd) => 'd) xa
+ ((split::('a => 'b => 'd) => 'a * 'b => 'd)
+ (%(xa::'a) y::'b. x (xb xa y)))))))"
by (import pair LET2_RAND)
-lemma LET2_RATOR: "ALL (x::'a1 * 'a2) (xa::'a1 => 'a2 => 'b => 'c) xb::'b.
- Let x (split xa) xb = (let (x::'a1, y::'a2) = x in xa x y xb)"
+lemma LET2_RATOR: "(All::('a1 * 'a2 => bool) => bool)
+ (%x::'a1 * 'a2.
+ (All::(('a1 => 'a2 => 'b => 'c) => bool) => bool)
+ (%xa::'a1 => 'a2 => 'b => 'c.
+ (All::('b => bool) => bool)
+ (%xb::'b.
+ (op =::'c => 'c => bool)
+ ((Let::'a1 * 'a2 => ('a1 * 'a2 => 'b => 'c) => 'b => 'c) x
+ ((split::('a1 => 'a2 => 'b => 'c)
+ => 'a1 * 'a2 => 'b => 'c)
+ xa)
+ xb)
+ ((Let::'a1 * 'a2 => ('a1 * 'a2 => 'c) => 'c) x
+ ((split::('a1 => 'a2 => 'c) => 'a1 * 'a2 => 'c)
+ (%(x::'a1) y::'a2. xa x y xb))))))"
by (import pair LET2_RATOR)
lemma pair_case_cong: "ALL x xa xb.
@@ -1116,10 +1157,10 @@
((Not::bool => bool) (P m)))))))"
by (import arithmetic WOP)
-lemma INV_PRE_LESS: "ALL m. 0 < m --> (ALL n. (PRE m < PRE n) = (m < n))"
+lemma INV_PRE_LESS: "ALL m>0. ALL n. (PRE m < PRE n) = (m < n)"
by (import arithmetic INV_PRE_LESS)
-lemma INV_PRE_LESS_EQ: "ALL n. 0 < n --> (ALL m. (PRE m <= PRE n) = (m <= n))"
+lemma INV_PRE_LESS_EQ: "ALL n>0. ALL m. (PRE m <= PRE n) = (m <= n)"
by (import arithmetic INV_PRE_LESS_EQ)
lemma SUB_EQ_EQ_0: "ALL (m::nat) n::nat. (m - n = m) = (m = (0::nat) | n = (0::nat))"
@@ -1282,7 +1323,7 @@
(0::nat) < n --> (EX (x::nat) q::nat. k = q * n + x & x < n)"
by (import arithmetic DA)
-lemma DIV_LESS_EQ: "ALL n::nat. (0::nat) < n --> (ALL k::nat. k div n <= k)"
+lemma DIV_LESS_EQ: "ALL n>0::nat. ALL k::nat. k div n <= k"
by (import arithmetic DIV_LESS_EQ)
lemma DIV_UNIQUE: "ALL (n::nat) (k::nat) q::nat.
@@ -1296,33 +1337,28 @@
lemma DIV_MULT: "ALL (n::nat) r::nat. r < n --> (ALL q::nat. (q * n + r) div n = q)"
by (import arithmetic DIV_MULT)
-lemma MOD_EQ_0: "ALL n::nat. (0::nat) < n --> (ALL k::nat. k * n mod n = (0::nat))"
+lemma MOD_EQ_0: "ALL n>0::nat. ALL k::nat. k * n mod n = (0::nat)"
by (import arithmetic MOD_EQ_0)
-lemma ZERO_MOD: "ALL n::nat. (0::nat) < n --> (0::nat) mod n = (0::nat)"
+lemma ZERO_MOD: "ALL n>0::nat. (0::nat) mod n = (0::nat)"
by (import arithmetic ZERO_MOD)
-lemma ZERO_DIV: "ALL n::nat. (0::nat) < n --> (0::nat) div n = (0::nat)"
+lemma ZERO_DIV: "ALL n>0::nat. (0::nat) div n = (0::nat)"
by (import arithmetic ZERO_DIV)
lemma MOD_MULT: "ALL (n::nat) r::nat. r < n --> (ALL q::nat. (q * n + r) mod n = r)"
by (import arithmetic MOD_MULT)
-lemma MOD_TIMES: "ALL n::nat.
- (0::nat) < n --> (ALL (q::nat) r::nat. (q * n + r) mod n = r mod n)"
+lemma MOD_TIMES: "ALL n>0::nat. ALL (q::nat) r::nat. (q * n + r) mod n = r mod n"
by (import arithmetic MOD_TIMES)
-lemma MOD_PLUS: "ALL n::nat.
- (0::nat) < n -->
- (ALL (j::nat) k::nat. (j mod n + k mod n) mod n = (j + k) mod n)"
+lemma MOD_PLUS: "ALL n>0::nat. ALL (j::nat) k::nat. (j mod n + k mod n) mod n = (j + k) mod n"
by (import arithmetic MOD_PLUS)
-lemma MOD_MOD: "ALL n::nat. (0::nat) < n --> (ALL k::nat. k mod n mod n = k mod n)"
+lemma MOD_MOD: "ALL n>0::nat. ALL k::nat. k mod n mod n = k mod n"
by (import arithmetic MOD_MOD)
-lemma ADD_DIV_ADD_DIV: "ALL x::nat.
- (0::nat) < x -->
- (ALL (xa::nat) r::nat. (xa * x + r) div x = xa + r div x)"
+lemma ADD_DIV_ADD_DIV: "ALL x>0::nat. ALL (xa::nat) r::nat. (xa * x + r) div x = xa + r div x"
by (import arithmetic ADD_DIV_ADD_DIV)
lemma MOD_MULT_MOD: "ALL (m::nat) n::nat.
@@ -1330,7 +1366,7 @@
(ALL x::nat. x mod (n * m) mod n = x mod n)"
by (import arithmetic MOD_MULT_MOD)
-lemma DIVMOD_ID: "ALL n::nat. (0::nat) < n --> n div n = (1::nat) & n mod n = (0::nat)"
+lemma DIVMOD_ID: "ALL n>0::nat. n div n = (1::nat) & n mod n = (0::nat)"
by (import arithmetic DIVMOD_ID)
lemma DIV_DIV_DIV_MULT: "ALL (x::nat) xa::nat.
@@ -1348,9 +1384,7 @@
P (p mod q) = (EX (k::nat) r::nat. p = k * q + r & r < q & P r)"
by (import arithmetic MOD_P)
-lemma MOD_TIMES2: "ALL n::nat.
- (0::nat) < n -->
- (ALL (j::nat) k::nat. j mod n * (k mod n) mod n = j * k mod n)"
+lemma MOD_TIMES2: "ALL n>0::nat. ALL (j::nat) k::nat. j mod n * (k mod n) mod n = j * k mod n"
by (import arithmetic MOD_TIMES2)
lemma MOD_COMMON_FACTOR: "ALL (n::nat) (p::nat) q::nat.
@@ -1362,7 +1396,7 @@
nat_case b f M = nat_case b' f' M'"
by (import arithmetic num_case_cong)
-lemma SUC_ELIM_THM: "ALL P. (ALL n. P (Suc n) n) = (ALL n. 0 < n --> P n (n - 1))"
+lemma SUC_ELIM_THM: "ALL P. (ALL n. P (Suc n) n) = (ALL n>0. P n (n - 1))"
by (import arithmetic SUC_ELIM_THM)
lemma SUB_ELIM_THM: "(P::nat => bool) ((a::nat) - (b::nat)) =
@@ -1375,7 +1409,7 @@
lemma MULT_INCREASES: "ALL m n. 1 < m & 0 < n --> Suc n <= m * n"
by (import arithmetic MULT_INCREASES)
-lemma EXP_ALWAYS_BIG_ENOUGH: "ALL b::nat. (1::nat) < b --> (ALL n::nat. EX m::nat. n <= b ^ m)"
+lemma EXP_ALWAYS_BIG_ENOUGH: "ALL b>1::nat. ALL n::nat. EX m::nat. n <= b ^ m"
by (import arithmetic EXP_ALWAYS_BIG_ENOUGH)
lemma EXP_EQ_0: "ALL (n::nat) m::nat. (n ^ m = (0::nat)) = (n = (0::nat) & (0::nat) < m)"
@@ -2449,7 +2483,7 @@
lemma NOT_LT_DIV: "ALL (a::nat) b::nat. (0::nat) < b & b < a --> ~ a dvd b"
by (import divides NOT_LT_DIV)
-lemma DIVIDES_FACT: "ALL b. 0 < b --> b dvd FACT b"
+lemma DIVIDES_FACT: "ALL b>0. b dvd FACT b"
by (import divides DIVIDES_FACT)
lemma DIVIDES_MULT_LEFT: "ALL (x::nat) xa::nat. (x * xa dvd xa) = (xa = (0::nat) | x = (1::nat))"
@@ -2661,9 +2695,21 @@
EL n (zip l1 l2) = (EL n l1, EL n l2)"
by (import list EL_ZIP)
-lemma MAP2_ZIP: "ALL l1 l2.
- length l1 = length l2 -->
- (ALL f. map2 f l1 l2 = map (split f) (zip l1 l2))"
+lemma MAP2_ZIP: "(All::('a list => bool) => bool)
+ (%l1::'a list.
+ (All::('b list => bool) => bool)
+ (%l2::'b list.
+ (op -->::bool => bool => bool)
+ ((op =::nat => nat => bool) ((size::'a list => nat) l1)
+ ((size::'b list => nat) l2))
+ ((All::(('a => 'b => 'c) => bool) => bool)
+ (%f::'a => 'b => 'c.
+ (op =::'c list => 'c list => bool)
+ ((map2::('a => 'b => 'c) => 'a list => 'b list => 'c list)
+ f l1 l2)
+ ((map::('a * 'b => 'c) => ('a * 'b) list => 'c list)
+ ((split::('a => 'b => 'c) => 'a * 'b => 'c) f)
+ ((zip::'a list => 'b list => ('a * 'b) list) l1 l2))))))"
by (import list MAP2_ZIP)
lemma MEM_EL: "(All::('a list => bool) => bool)
@@ -4260,9 +4306,6 @@
lemma NULL_FOLDL: "ALL l. null l = foldl (%x l'. False) True l"
by (import rich_list NULL_FOLDL)
-lemma FILTER_REVERSE: "ALL P l. filter P (rev l) = rev (filter P l)"
- by (import rich_list FILTER_REVERSE)
-
lemma SEG_LENGTH_ID: "ALL l. SEG (length l) 0 l = l"
by (import rich_list SEG_LENGTH_ID)
@@ -4539,7 +4582,7 @@
lemma ELL_0_SNOC: "ALL l x. ELL 0 (SNOC x l) = x"
by (import rich_list ELL_0_SNOC)
-lemma ELL_SNOC: "ALL n. 0 < n --> (ALL x l. ELL n (SNOC x l) = ELL (PRE n) l)"
+lemma ELL_SNOC: "ALL n>0. ALL x l. ELL n (SNOC x l) = ELL (PRE n) l"
by (import rich_list ELL_SNOC)
lemma ELL_SUC_SNOC: "ALL n x xa. ELL (Suc n) (SNOC x xa) = ELL n xa"
@@ -4615,9 +4658,6 @@
lemma FLAT_FLAT: "ALL l. concat (concat l) = concat (map concat l)"
by (import rich_list FLAT_FLAT)
-lemma ALL_EL_REVERSE: "ALL P l. list_all P (rev l) = list_all P l"
- by (import rich_list ALL_EL_REVERSE)
-
lemma SOME_EL_REVERSE: "ALL P l. list_exists P (rev l) = list_exists P l"
by (import rich_list SOME_EL_REVERSE)
@@ -4735,7 +4775,7 @@
lemma EL_MAP: "ALL n l. n < length l --> (ALL f. EL n (map f l) = f (EL n l))"
by (import rich_list EL_MAP)
-lemma EL_CONS: "ALL n. 0 < n --> (ALL x l. EL n (x # l) = EL (PRE n) l)"
+lemma EL_CONS: "ALL n>0. ALL x l. EL n (x # l) = EL (PRE n) l"
by (import rich_list EL_CONS)
lemma EL_SEG: "ALL n l. n < length l --> EL n l = hd (SEG 1 n l)"
@@ -4805,7 +4845,7 @@
lemma LENGTH_REPLICATE: "ALL n x. length (REPLICATE n x) = n"
by (import rich_list LENGTH_REPLICATE)
-lemma IS_EL_REPLICATE: "ALL n. 0 < n --> (ALL x. x mem REPLICATE n x)"
+lemma IS_EL_REPLICATE: "ALL n>0. ALL x. x mem REPLICATE n x"
by (import rich_list IS_EL_REPLICATE)
lemma ALL_EL_REPLICATE: "ALL x n. list_all (op = x) (REPLICATE n x)"
@@ -4837,9 +4877,24 @@
constdefs
BIND :: "('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a"
- "BIND == %g f. split f o g"
-
-lemma BIND_DEF: "ALL g f. BIND g f = split f o g"
+ "(op ==::(('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a)
+ => (('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a)
+ => prop)
+ (BIND::('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a)
+ (%(g::'a => 'b * 'a) f::'b => 'a => 'c * 'a.
+ (op o::('b * 'a => 'c * 'a) => ('a => 'b * 'a) => 'a => 'c * 'a)
+ ((split::('b => 'a => 'c * 'a) => 'b * 'a => 'c * 'a) f) g)"
+
+lemma BIND_DEF: "(All::(('a => 'b * 'a) => bool) => bool)
+ (%g::'a => 'b * 'a.
+ (All::(('b => 'a => 'c * 'a) => bool) => bool)
+ (%f::'b => 'a => 'c * 'a.
+ (op =::('a => 'c * 'a) => ('a => 'c * 'a) => bool)
+ ((BIND::('a => 'b * 'a)
+ => ('b => 'a => 'c * 'a) => 'a => 'c * 'a)
+ g f)
+ ((op o::('b * 'a => 'c * 'a) => ('a => 'b * 'a) => 'a => 'c * 'a)
+ ((split::('b => 'a => 'c * 'a) => 'b * 'a => 'c * 'a) f) g)))"
by (import state_transformer BIND_DEF)
constdefs
--- a/src/HOL/Import/HOL/HOL4Prob.thy Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Fri Apr 01 18:59:17 2005 +0200
@@ -1,3 +1,5 @@
+(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
+
theory HOL4Prob = HOL4Real:
;setup_theory prob_extra
@@ -26,10 +28,10 @@
((op +::nat => nat => nat)
((op *::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
q)
r))
((op |::bool => bool => bool)
@@ -39,17 +41,17 @@
((op =::nat => nat => bool) q
((op div::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op =::nat => nat => bool) r
((op mod::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))))))"
by (import prob_extra DIV_TWO_UNIQUE)
lemma DIVISION_TWO: "ALL n::nat.
@@ -75,16 +77,16 @@
((op <::nat => nat => bool)
((op div::nat => nat => nat) m
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
((op div::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op <::nat => nat => bool) m n)))"
by (import prob_extra DIV_TWO_MONO)
@@ -97,16 +99,16 @@
((op <::nat => nat => bool)
((op div::nat => nat => nat) m
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
((op div::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op <::nat => nat => bool) m n))))"
by (import prob_extra DIV_TWO_MONO_EVEN)
@@ -203,18 +205,18 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
n)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
m))))"
by (import prob_extra POW_HALF_MONO)
@@ -2527,10 +2529,10 @@
((op *::real => real => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
((prob::((nat => bool) => bool) => real) p)))))"
by (import prob PROB_INTER_SHD)
@@ -3155,10 +3157,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+ (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit))))
((size::bool list => nat) x))
((prob::((nat => bool) => bool) => real) q))))))))"
by (import prob_indep INDEP_INDEP_SET_LEMMA)
@@ -3381,10 +3383,10 @@
(op -->::bool => bool => bool)
(P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
(P ((Suc::nat => nat) v)))))
((All::(nat => bool) => bool) P))"
by (import prob_uniform unif_bound_ind)
@@ -3435,10 +3437,10 @@
(op -->::bool => bool => bool)
(P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
s)
(P ((Suc::nat => nat) v2) s)))))
((All::(nat => bool) => bool)
@@ -3715,15 +3717,15 @@
((op <=::nat => nat => bool)
((op ^::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))
((unif_bound::nat => nat) n))
((op *::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))
n)))"
by (import prob_uniform UNIF_BOUND_UPPER)
@@ -3770,10 +3772,10 @@
((op <=::nat => nat => bool) k
((op ^::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
((unif_bound::nat => nat) n)))
((op =::real => real => bool)
((prob::((nat => bool) => bool) => real)
@@ -3787,10 +3789,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
((unif_bound::nat => nat) n))))))"
by (import prob_uniform PROB_UNIF_BOUND)
@@ -3906,10 +3908,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+ (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit))))
t))))))"
by (import prob_uniform PROB_UNIFORM_PAIR_SUC)
@@ -3937,10 +3939,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
t)))))"
by (import prob_uniform PROB_UNIFORM_SUC)
@@ -3968,10 +3970,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
t)))))"
by (import prob_uniform PROB_UNIFORM)
--- a/src/HOL/Import/HOL/HOL4Real.thy Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy Fri Apr 01 18:59:17 2005 +0200
@@ -1,3 +1,5 @@
+(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
+
theory HOL4Real = HOL4Base:
;setup_theory realax
@@ -254,9 +256,6 @@
lemma REAL_LT_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y < x)"
by (import real REAL_LT_ANTISYM)
-lemma REAL_LET_TOTAL: "ALL (x::real) y::real. x <= y | y < x"
- by (import real REAL_LET_TOTAL)
-
lemma REAL_LTE_TOTAL: "ALL (x::real) y::real. x < y | y <= x"
by (import real REAL_LTE_TOTAL)
@@ -284,6 +283,12 @@
lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x - y) = x"
by (import real REAL_SUB_ADD2)
+lemma REAL_SUB_LT: "ALL (x::real) y::real. ((0::real) < x - y) = (y < x)"
+ by (import real REAL_SUB_LT)
+
+lemma REAL_SUB_LE: "ALL (x::real) y::real. ((0::real) <= x - y) = (y <= x)"
+ by (import real REAL_SUB_LE)
+
lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y - x = y"
by (import real REAL_ADD_SUB)
@@ -307,7 +312,7 @@
lemma REAL_LINV_UNIQ: "ALL (x::real) y::real. x * y = (1::real) --> x = inverse y"
by (import real REAL_LINV_UNIQ)
-lemma REAL_LE_INV: "ALL x::real. (0::real) <= x --> (0::real) <= inverse x"
+lemma REAL_LE_INV: "ALL x>=0::real. (0::real) <= inverse x"
by (import real REAL_LE_INV)
lemma REAL_LE_ADDR: "ALL (x::real) y::real. (x <= x + y) = ((0::real) <= y)"
@@ -355,7 +360,7 @@
lemma REAL_DIV_RMUL: "ALL (x::real) y::real. y ~= (0::real) --> x / y * y = x"
by (import real REAL_DIV_RMUL)
-lemma REAL_DOWN: "ALL x::real. (0::real) < x --> (EX xa::real. (0::real) < xa & xa < x)"
+lemma REAL_DOWN: "ALL x>0::real. EX xa>0::real. xa < x"
by (import real REAL_DOWN)
lemma REAL_SUB_SUB: "ALL (x::real) y::real. x - y - x = - y"
@@ -417,7 +422,7 @@
lemma REAL_LT_1: "ALL (x::real) y::real. (0::real) <= x & x < y --> x / y < (1::real)"
by (import real REAL_LT_1)
-lemma REAL_POS_NZ: "ALL x::real. (0::real) < x --> x ~= (0::real)"
+lemma REAL_POS_NZ: "ALL x>0::real. x ~= (0::real)"
by (import real REAL_POS_NZ)
lemma REAL_EQ_LMUL_IMP: "ALL (x::real) (xa::real) xb::real.
@@ -447,9 +452,6 @@
abs w < y & abs x < z --> abs (w * x) < y * z"
by (import real ABS_LT_MUL2)
-lemma ABS_SUB: "ALL (x::real) y::real. abs (x - y) = abs (y - x)"
- by (import real ABS_SUB)
-
lemma ABS_REFL: "ALL x::real. (abs x = x) = ((0::real) <= x)"
by (import real ABS_REFL)
@@ -492,16 +494,16 @@
x < y"
by (import real ABS_BETWEEN2)
-lemma POW_PLUS1: "ALL e. 0 < e --> (ALL n. 1 + real n * e <= (1 + e) ^ n)"
+lemma POW_PLUS1: "ALL e>0. ALL n. 1 + real n * e <= (1 + e) ^ n"
by (import real POW_PLUS1)
lemma POW_M1: "ALL n::nat. abs ((- (1::real)) ^ n) = (1::real)"
by (import real POW_M1)
-lemma REAL_LE1_POW2: "ALL x::real. (1::real) <= x --> (1::real) <= x ^ 2"
+lemma REAL_LE1_POW2: "ALL x>=1::real. (1::real) <= x ^ 2"
by (import real REAL_LE1_POW2)
-lemma REAL_LT1_POW2: "ALL x::real. (1::real) < x --> (1::real) < x ^ 2"
+lemma REAL_LT1_POW2: "ALL x>1::real. (1::real) < x ^ 2"
by (import real REAL_LT1_POW2)
lemma POW_POS_LT: "ALL (x::real) n::nat. (0::real) < x --> (0::real) < x ^ Suc n"
@@ -571,9 +573,7 @@
lemma REAL_SUP_UBOUND_LE: "ALL P. Ex P & (EX z. ALL x. P x --> x <= z) --> (ALL y. P y --> y <= sup P)"
by (import real REAL_SUP_UBOUND_LE)
-lemma REAL_ARCH_LEAST: "ALL y.
- 0 < y -->
- (ALL x. 0 <= x --> (EX n. real n * y <= x & x < real (Suc n) * y))"
+lemma REAL_ARCH_LEAST: "ALL y>0. ALL x>=0. EX n. real n * y <= x & x < real (Suc n) * y"
by (import real REAL_ARCH_LEAST)
consts
@@ -587,7 +587,12 @@
sum :: "nat * nat => (nat => real) => real"
defs
- sum_def: "real.sum == split sumc"
+ sum_def: "(op ==::(nat * nat => (nat => real) => real)
+ => (nat * nat => (nat => real) => real) => prop)
+ (real.sum::nat * nat => (nat => real) => real)
+ ((split::(nat => nat => (nat => real) => real)
+ => nat * nat => (nat => real) => real)
+ (sumc::nat => nat => (nat => real) => real))"
lemma SUM_DEF: "ALL m n f. real.sum (m, n) f = sumc m n f"
by (import real SUM_DEF)
@@ -913,25 +918,22 @@
mtop :: "'a metric => 'a topology"
"mtop ==
%m. topology
- (%S'. ALL x.
- S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))"
+ (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))"
lemma mtop: "ALL m.
mtop m =
topology
- (%S'. ALL x.
- S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))"
+ (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))"
by (import topology mtop)
lemma mtop_istopology: "ALL m.
istopology
- (%S'. ALL x.
- S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))"
+ (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))"
by (import topology mtop_istopology)
lemma MTOP_OPEN: "ALL S' x.
open (mtop x) S' =
- (ALL xa. S' xa --> (EX e. 0 < e & (ALL y. dist x (xa, y) < e --> S' y)))"
+ (ALL xa. S' xa --> (EX e>0. ALL y. dist x (xa, y) < e --> S' y))"
by (import topology MTOP_OPEN)
constdefs
@@ -948,8 +950,7 @@
by (import topology BALL_NEIGH)
lemma MTOP_LIMPT: "ALL m x S'.
- limpt (mtop m) x S' =
- (ALL e. 0 < e --> (EX y. x ~= y & S' y & dist m (x, y) < e))"
+ limpt (mtop m) x S' = (ALL e>0. EX y. x ~= y & S' y & dist m (x, y) < e)"
by (import topology MTOP_LIMPT)
lemma ISMET_R1: "ismet (%(x, y). abs (y - x))"
@@ -1054,8 +1055,7 @@
lemma MTOP_TENDS: "ALL d g x x0.
tends x x0 (mtop d, g) =
- (ALL e.
- 0 < e --> (EX n. g n n & (ALL m. g m n --> dist d (x m, x0) < e)))"
+ (ALL e>0. EX n. g n n & (ALL m. g m n --> dist d (x m, x0) < e))"
by (import nets MTOP_TENDS)
lemma MTOP_TENDS_UNIQ: "ALL (g::'b => 'b => bool) d::'a metric.
@@ -1067,29 +1067,27 @@
lemma SEQ_TENDS: "ALL d x x0.
tends x x0 (mtop d, nat_ge) =
- (ALL xa. 0 < xa --> (EX xb. ALL xc. xb <= xc --> dist d (x xc, x0) < xa))"
+ (ALL xa>0. EX xb. ALL xc. xb <= xc --> dist d (x xc, x0) < xa)"
by (import nets SEQ_TENDS)
lemma LIM_TENDS: "ALL m1 m2 f x0 y0.
limpt (mtop m1) x0 re_universe -->
tends f y0 (mtop m2, tendsto (m1, x0)) =
- (ALL e.
- 0 < e -->
- (EX d. 0 < d &
- (ALL x.
- 0 < dist m1 (x, x0) & dist m1 (x, x0) <= d -->
- dist m2 (f x, y0) < e)))"
+ (ALL e>0.
+ EX d>0.
+ ALL x.
+ 0 < dist m1 (x, x0) & dist m1 (x, x0) <= d -->
+ dist m2 (f x, y0) < e)"
by (import nets LIM_TENDS)
lemma LIM_TENDS2: "ALL m1 m2 f x0 y0.
limpt (mtop m1) x0 re_universe -->
tends f y0 (mtop m2, tendsto (m1, x0)) =
- (ALL e.
- 0 < e -->
- (EX d. 0 < d &
- (ALL x.
- 0 < dist m1 (x, x0) & dist m1 (x, x0) < d -->
- dist m2 (f x, y0) < e)))"
+ (ALL e>0.
+ EX d>0.
+ ALL x.
+ 0 < dist m1 (x, x0) & dist m1 (x, x0) < d -->
+ dist m2 (f x, y0) < e)"
by (import nets LIM_TENDS2)
lemma MR1_BOUNDED: "ALL g f.
@@ -1915,16 +1913,16 @@
((Pair::nat => nat => nat * nat)
((op *::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
n)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
f)
((suminf::(nat => real) => real) f)))"
by (import seq SER_PAIR)
@@ -1956,19 +1954,19 @@
(f ((op +::nat => nat => nat) n
((op *::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+ (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))
d)))
(f ((op +::nat => nat => nat) n
((op +::nat => nat => nat)
((op *::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+ (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))
d)
(1::nat))))))))
((op <::real => real => bool)
@@ -2824,10 +2822,10 @@
((uminus::real => real)
((op ^::real => nat => real) ((inverse::real => real) x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x))"
by (import lim DIFF_XM1)
@@ -2848,10 +2846,10 @@
((op /::real => real => real) l
((op ^::real => nat => real) (f x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
x))))"
by (import lim DIFF_INV)
@@ -2885,10 +2883,10 @@
((op *::real => real => real) m (f x)))
((op ^::real => nat => real) (g x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
-(Numeral.Pls::bin) (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+(Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))))
x))))))"
by (import lim DIFF_DIV)
@@ -3869,9 +3867,9 @@
((op -::nat => nat => nat)
((op -::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit))))
p)
q)))))))))))"
by (import powser TERMDIFF_LEMMA2)
@@ -3916,10 +3914,10 @@
((op ^::real => nat => real) k'
((op -::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+ (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))))
((abs::real => real) h)))))))))"
by (import powser TERMDIFF_LEMMA3)
@@ -4112,10 +4110,10 @@
((op /::real => real => real) l
((op ^::real => nat => real) (f x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
x))
((op &::bool => bool => bool)
((op -->::bool => bool => bool)
@@ -4134,10 +4132,10 @@
((op *::real => real => real) m (f x)))
((op ^::real => nat => real) (g x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x))
((op &::bool => bool => bool)
((op -->::bool => bool => bool)
@@ -4212,19 +4210,10 @@
lemma EXP_0: "exp 0 = 1"
by (import transc EXP_0)
-lemma EXP_LE_X: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) x)
- ((op <=::real => real => bool)
- ((op +::real => real => real) (1::real) x) ((exp::real => real) x)))"
+lemma EXP_LE_X: "ALL x>=0. 1 + x <= exp x"
by (import transc EXP_LE_X)
-lemma EXP_LT_1: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <::real => real => bool) (0::real) x)
- ((op <::real => real => bool) (1::real) ((exp::real => real) x)))"
+lemma EXP_LT_1: "ALL x>0. 1 < exp x"
by (import transc EXP_LT_1)
lemma EXP_ADD_MUL: "ALL x y. exp (x + y) * exp (- x) = exp y"
@@ -4275,26 +4264,10 @@
lemma EXP_INJ: "ALL x y. (exp x = exp y) = (x = y)"
by (import transc EXP_INJ)
-lemma EXP_TOTAL_LEMMA: "(All::(real => bool) => bool)
- (%y::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (1::real) y)
- ((Ex::(real => bool) => bool)
- (%x::real.
- (op &::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) x)
- ((op &::bool => bool => bool)
- ((op <=::real => real => bool) x
- ((op -::real => real => real) y (1::real)))
- ((op =::real => real => bool) ((exp::real => real) x) y)))))"
+lemma EXP_TOTAL_LEMMA: "ALL y>=1. EX x>=0. x <= y - 1 & exp x = y"
by (import transc EXP_TOTAL_LEMMA)
-lemma EXP_TOTAL: "(All::(real => bool) => bool)
- (%y::real.
- (op -->::bool => bool => bool)
- ((op <::real => real => bool) (0::real) y)
- ((Ex::(real => bool) => bool)
- (%x::real. (op =::real => real => bool) ((exp::real => real) x) y)))"
+lemma EXP_TOTAL: "ALL y>0. EX x. exp x = y"
by (import transc EXP_TOTAL)
constdefs
@@ -4341,13 +4314,7 @@
lemma LN_1: "ln 1 = 0"
by (import transc LN_1)
-lemma LN_INV: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <::real => real => bool) (0::real) x)
- ((op =::real => real => bool)
- ((ln::real => real) ((inverse::real => real) x))
- ((uminus::real => real) ((ln::real => real) x))))"
+lemma LN_INV: "ALL x>0. ln (inverse x) = - ln x"
by (import transc LN_INV)
lemma LN_DIV: "(All::(real => bool) => bool)
@@ -4404,26 +4371,13 @@
((ln::real => real) x)))))"
by (import transc LN_POW)
-lemma LN_LE: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) x)
- ((op <=::real => real => bool)
- ((ln::real => real) ((op +::real => real => real) (1::real) x)) x))"
+lemma LN_LE: "ALL x>=0. ln (1 + x) <= x"
by (import transc LN_LE)
-lemma LN_LT_X: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <::real => real => bool) (0::real) x)
- ((op <::real => real => bool) ((ln::real => real) x) x))"
+lemma LN_LT_X: "ALL x>0. ln x < x"
by (import transc LN_LT_X)
-lemma LN_POS: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (1::real) x)
- ((op <=::real => real => bool) (0::real) ((ln::real => real) x)))"
+lemma LN_POS: "ALL x>=1. 0 <= ln x"
by (import transc LN_POS)
constdefs
@@ -4630,34 +4584,16 @@
lemma SQRT_1: "sqrt 1 = 1"
by (import transc SQRT_1)
-lemma SQRT_POS_LT: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <::real => real => bool) (0::real) x)
- ((op <::real => real => bool) (0::real) ((sqrt::real => real) x)))"
+lemma SQRT_POS_LT: "ALL x>0. 0 < sqrt x"
by (import transc SQRT_POS_LT)
-lemma SQRT_POS_LE: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) x)
- ((op <=::real => real => bool) (0::real) ((sqrt::real => real) x)))"
+lemma SQRT_POS_LE: "ALL x>=0. 0 <= sqrt x"
by (import transc SQRT_POS_LE)
lemma SQRT_POW2: "ALL x. (sqrt x ^ 2 = x) = (0 <= x)"
by (import transc SQRT_POW2)
-lemma SQRT_POW_2: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) x)
- ((op =::real => real => bool)
- ((op ^::real => nat => real) ((sqrt::real => real) x)
- ((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool))))
- x))"
+lemma SQRT_POW_2: "ALL x>=0. sqrt x ^ 2 = x"
by (import transc SQRT_POW_2)
lemma POW_2_SQRT: "(op -->::bool => bool => bool)
@@ -4666,9 +4602,9 @@
((sqrt::real => real)
((op ^::real => nat => real) x
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))))
x)"
by (import transc POW_2_SQRT)
@@ -4684,10 +4620,10 @@
((op =::real => real => bool)
((op ^::real => nat => real) xa
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
x)))
((op =::real => real => bool) ((sqrt::real => real) x) xa)))"
by (import transc SQRT_POS_UNIQ)
@@ -4706,13 +4642,7 @@
((sqrt::real => real) xa)))))"
by (import transc SQRT_MUL)
-lemma SQRT_INV: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) x)
- ((op =::real => real => bool)
- ((sqrt::real => real) ((inverse::real => real) x))
- ((inverse::real => real) ((sqrt::real => real) x))))"
+lemma SQRT_INV: "ALL x>=0. sqrt (inverse x) = inverse (sqrt x)"
by (import transc SQRT_INV)
lemma SQRT_DIV: "(All::(real => bool) => bool)
@@ -4748,31 +4678,25 @@
((sqrt::real => real)
((op ^::real => nat => real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
n))
((op ^::real => nat => real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))
((op div::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))))"
by (import transc SQRT_EVEN_POW2)
-lemma REAL_DIV_SQRT: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) x)
- ((op =::real => real => bool)
- ((op /::real => real => real) x ((sqrt::real => real) x))
- ((sqrt::real => real) x)))"
+lemma REAL_DIV_SQRT: "ALL x>=0. x / sqrt x = sqrt x"
by (import transc REAL_DIV_SQRT)
lemma SQRT_EQ: "(All::(real => bool) => bool)
@@ -4784,10 +4708,10 @@
((op =::real => real => bool)
((op ^::real => nat => real) x
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
y)
((op <=::real => real => bool) (0::real) x))
((op =::real => real => bool) x ((sqrt::real => real) y))))"
@@ -4852,9 +4776,9 @@
((op <::real => real => bool) (0::real) x)
((op <::real => real => bool) x
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))))
((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
by (import transc SIN_POS)
@@ -4927,10 +4851,10 @@
((op <::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
by (import transc SIN_POS_PI2)
@@ -4942,10 +4866,10 @@
((op <::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
by (import transc COS_POS_PI2)
@@ -4957,18 +4881,18 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x)
((op <::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
by (import transc COS_POS_PI)
@@ -4989,10 +4913,10 @@
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
by (import transc COS_POS_PI2_LE)
@@ -5004,18 +4928,18 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x)
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
by (import transc COS_POS_PI_LE)
@@ -5027,10 +4951,10 @@
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op <=::real => real => bool) (0::real) ((sin::real => real) x)))"
by (import transc SIN_POS_PI2_LE)
@@ -5071,19 +4995,19 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x)
((op &::bool => bool => bool)
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op =::real => real => bool) ((sin::real => real) x) y)))))"
by (import transc SIN_TOTAL)
@@ -5101,10 +5025,10 @@
((op *::real => real => real) ((real::nat => real) n)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))))))"
by (import transc COS_ZERO_LEMMA)
lemma SIN_ZERO_LEMMA: "(All::(real => bool) => bool)
@@ -5120,10 +5044,10 @@
((op *::real => real => real) ((real::nat => real) n)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))))))"
by (import transc SIN_ZERO_LEMMA)
lemma COS_ZERO: "ALL x.
@@ -5198,36 +5122,36 @@
((cos::real => real)
((op *::real => real => real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
x))
(0::real))))
((op =::real => real => bool)
((tan::real => real)
((op *::real => real => real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
x))
((op /::real => real => real)
((op *::real => real => real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
((tan::real => real) x))
((op -::real => real => real) (1::real)
((op ^::real => nat => real) ((tan::real => real) x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))))"
by (import transc TAN_DOUBLE)
lemma TAN_POS_PI2: "(All::(real => bool) => bool)
@@ -5238,10 +5162,10 @@
((op <::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op <::real => real => bool) (0::real) ((tan::real => real) x)))"
by (import transc TAN_POS_PI2)
@@ -5254,49 +5178,17 @@
((inverse::real => real)
((op ^::real => nat => real) ((cos::real => real) x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x))"
by (import transc DIFF_TAN)
-lemma TAN_TOTAL_LEMMA: "(All::(real => bool) => bool)
- (%y::real.
- (op -->::bool => bool => bool)
- ((op <::real => real => bool) (0::real) y)
- ((Ex::(real => bool) => bool)
- (%x::real.
- (op &::bool => bool => bool)
- ((op <::real => real => bool) (0::real) x)
- ((op &::bool => bool => bool)
- ((op <::real => real => bool) x
- ((op /::real => real => real) (pi::real)
- ((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
- ((op <::real => real => bool) y ((tan::real => real) x))))))"
+lemma TAN_TOTAL_LEMMA: "ALL y>0. EX x>0. x < pi / 2 & y < tan x"
by (import transc TAN_TOTAL_LEMMA)
-lemma TAN_TOTAL_POS: "(All::(real => bool) => bool)
- (%y::real.
- (op -->::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) y)
- ((Ex::(real => bool) => bool)
- (%x::real.
- (op &::bool => bool => bool)
- ((op <=::real => real => bool) (0::real) x)
- ((op &::bool => bool => bool)
- ((op <::real => real => bool) x
- ((op /::real => real => real) (pi::real)
- ((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
- ((op =::real => real => bool) ((tan::real => real) x) y)))))"
+lemma TAN_TOTAL_POS: "ALL y>=0. EX x>=0. x < pi / 2 & tan x = y"
by (import transc TAN_TOTAL_POS)
lemma TAN_TOTAL: "ALL y. EX! x. - (pi / 2) < x & x < pi / 2 & tan x = y"
@@ -5334,19 +5226,19 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((asn::real => real) y))
((op &::bool => bool => bool)
((op <=::real => real => bool) ((asn::real => real) y)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op =::real => real => bool)
((sin::real => real) ((asn::real => real) y)) y))))"
by (import transc ASN)
@@ -5372,18 +5264,18 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((asn::real => real) y))
((op <=::real => real => bool) ((asn::real => real) y)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))))"
by (import transc ASN_BOUNDS)
lemma ASN_BOUNDS_LT: "(All::(real => bool) => bool)
@@ -5397,18 +5289,18 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((asn::real => real) y))
((op <::real => real => bool) ((asn::real => real) y)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))))"
by (import transc ASN_BOUNDS_LT)
lemma SIN_ASN: "(All::(real => bool) => bool)
@@ -5419,18 +5311,18 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x)
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op =::real => real => bool)
((asn::real => real) ((sin::real => real) x)) x))"
by (import transc SIN_ASN)
@@ -5508,18 +5400,18 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x)
((op <::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op =::real => real => bool)
((atn::real => real) ((tan::real => real) x)) x))"
by (import transc TAN_ATN)
@@ -5533,16 +5425,16 @@
((op +::real => real => real) (1::real)
((op ^::real => nat => real) ((tan::real => real) x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op ^::real => nat => real)
((inverse::real => real) ((cos::real => real) x))
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit))))))"
by (import transc TAN_SEC)
lemma SIN_COS_SQ: "(All::(real => bool) => bool)
@@ -5556,10 +5448,10 @@
((op -::real => real => real) (1::real)
((op ^::real => nat => real) ((cos::real => real) x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))))"
by (import transc SIN_COS_SQ)
lemma COS_SIN_SQ: "(All::(real => bool) => bool)
@@ -5570,27 +5462,27 @@
((uminus::real => real)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
x)
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))
((op =::real => real => bool) ((cos::real => real) x)
((sqrt::real => real)
((op -::real => real => real) (1::real)
((op ^::real => nat => real) ((sin::real => real) x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))))"
by (import transc COS_SIN_SQ)
lemma COS_ATN_NZ: "ALL x. cos (atn x) ~= 0"
@@ -5627,10 +5519,10 @@
((op -::real => real => real) (1::real)
((op ^::real => nat => real) ((sin::real => real) x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))))"
by (import transc COS_SIN_SQRT)
lemma SIN_COS_SQRT: "(All::(real => bool) => bool)
@@ -5642,18 +5534,13 @@
((op -::real => real => real) (1::real)
((op ^::real => nat => real) ((cos::real => real) x)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))))"
by (import transc SIN_COS_SQRT)
-lemma DIFF_LN: "(All::(real => bool) => bool)
- (%x::real.
- (op -->::bool => bool => bool)
- ((op <::real => real => bool) (0::real) x)
- ((diffl::(real => real) => real => real => bool) (ln::real => real)
- ((inverse::real => real) x) x))"
+lemma DIFF_LN: "ALL x>0. diffl ln (inverse x) x"
by (import transc DIFF_LN)
lemma DIFF_ASN_LEMMA: "(All::(real => bool) => bool)
@@ -5680,10 +5567,10 @@
((op -::real => real => real) (1::real)
((op ^::real => nat => real) x
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))))
x))"
by (import transc DIFF_ASN)
@@ -5713,10 +5600,10 @@
((op -::real => real => real) (1::real)
((op ^::real => nat => real) x
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))))))
x))"
by (import transc DIFF_ACS)
--- a/src/HOL/Import/HOL/HOL4Vec.thy Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Fri Apr 01 18:59:17 2005 +0200
@@ -1,3 +1,5 @@
+(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
+
theory HOL4Vec = HOL4Base:
;setup_theory res_quan
@@ -1102,9 +1104,9 @@
(op -->::bool => bool => bool)
((op <::nat => nat => bool) x
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit))))
((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
x))"
by (import bword_num BV_VB)
@@ -1157,8 +1159,7 @@
lemma NBWORD_SUC_WSEG: "ALL n. RES_FORALL (PWORDLEN (Suc n)) (%w. NBWORD n (BNVAL w) = WSEG n 0 w)"
by (import bword_num NBWORD_SUC_WSEG)
-lemma DOUBL_EQ_SHL: "ALL x.
- 0 < x -->
+lemma DOUBL_EQ_SHL: "ALL x>0.
RES_FORALL (PWORDLEN x)
(%xa. ALL xb.
NBWORD x (BNVAL xa + BNVAL xa + BV xb) = snd (SHL False xa xb))"
@@ -1297,10 +1298,10 @@
((BV::bool => nat) cin))
((op ^::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+ (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))
k)))))))"
by (import bword_arith ACARRY_EQ_ADD_DIV)
--- a/src/HOL/Import/HOL/HOL4Word32.thy Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Fri Apr 01 18:59:17 2005 +0200
@@ -1,3 +1,5 @@
+(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
+
theory HOL4Word32 = HOL4Base:
;setup_theory bits
@@ -293,22 +295,17 @@
~ oper (bit x a) (bit x b) --> BITWISE n oper a b div 2 ^ x mod 2 = 0"
by (import bits BITWISE_NOT_COR)
-lemma MOD_PLUS_RIGHT: "ALL n::nat.
- (0::nat) < n -->
- (ALL (j::nat) k::nat. (j + k mod n) mod n = (j + k) mod n)"
+lemma MOD_PLUS_RIGHT: "ALL n>0::nat. ALL (j::nat) k::nat. (j + k mod n) mod n = (j + k) mod n"
by (import bits MOD_PLUS_RIGHT)
-lemma MOD_PLUS_1: "ALL n::nat.
- (0::nat) < n -->
- (ALL x::nat.
- ((x + (1::nat)) mod n = (0::nat)) = (x mod n + (1::nat) = n))"
+lemma MOD_PLUS_1: "ALL n>0::nat.
+ ALL x::nat. ((x + (1::nat)) mod n = (0::nat)) = (x mod n + (1::nat) = n)"
by (import bits MOD_PLUS_1)
-lemma MOD_ADD_1: "ALL n::nat.
- (0::nat) < n -->
- (ALL x::nat.
- (x + (1::nat)) mod n ~= (0::nat) -->
- (x + (1::nat)) mod n = x mod n + (1::nat))"
+lemma MOD_ADD_1: "ALL n>0::nat.
+ ALL x::nat.
+ (x + (1::nat)) mod n ~= (0::nat) -->
+ (x + (1::nat)) mod n = x mod n + (1::nat)"
by (import bits MOD_ADD_1)
;end_setup
--- a/src/HOL/Import/HOL/ROOT.ML Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML Fri Apr 01 18:59:17 2005 +0200
@@ -3,7 +3,5 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-with_path ".." use_thy "HOL4Compat";
-with_path ".." use_thy "HOL4Syntax";
setmp quick_and_dirty true use_thy "HOL4Prob";
setmp quick_and_dirty true use_thy "HOL4";
--- a/src/HOL/Import/HOL/arithmetic.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp Fri Apr 01 18:59:17 2005 +0200
@@ -15,8 +15,8 @@
"NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
"NUMERAL" > "HOL4Compat.NUMERAL"
"MOD" > "Divides.op mod" :: "nat => nat => nat"
- "MIN" > "HOL.min" :: "nat => nat => nat"
- "MAX" > "HOL.max" :: "nat => nat => nat"
+ "MIN" > "Orderings.min" :: "nat => nat => nat"
+ "MAX" > "Orderings.max" :: "nat => nat => nat"
"FUNPOW" > "HOL4Compat.FUNPOW"
"EXP" > "Nat.power" :: "nat => nat => nat"
"DIV" > "Divides.op div" :: "nat => nat => nat"
@@ -141,17 +141,17 @@
"MIN_MAX_EQ" > "HOL4Base.arithmetic.MIN_MAX_EQ"
"MIN_LT" > "HOL4Base.arithmetic.MIN_LT"
"MIN_LE" > "HOL4Base.arithmetic.MIN_LE"
- "MIN_IDEM" > "HOL.min_same"
+ "MIN_IDEM" > "Orderings.min_same"
"MIN_DEF" > "HOL4Compat.MIN_DEF"
- "MIN_COMM" > "HOL.min_ac_2"
- "MIN_ASSOC" > "HOL.min_ac_1"
+ "MIN_COMM" > "Orderings.min_ac_2"
+ "MIN_ASSOC" > "Orderings.min_ac_1"
"MIN_0" > "HOL4Base.arithmetic.MIN_0"
"MAX_LT" > "HOL4Base.arithmetic.MAX_LT"
"MAX_LE" > "HOL4Base.arithmetic.MAX_LE"
- "MAX_IDEM" > "HOL.max_same"
+ "MAX_IDEM" > "Orderings.max_same"
"MAX_DEF" > "HOL4Compat.MAX_DEF"
- "MAX_COMM" > "HOL.max_ac_2"
- "MAX_ASSOC" > "HOL.max_ac_1"
+ "MAX_COMM" > "Orderings.max_ac_2"
+ "MAX_ASSOC" > "Orderings.max_ac_1"
"MAX_0" > "HOL4Base.arithmetic.MAX_0"
"LESS_TRANS" > "Nat.less_trans"
"LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT"
@@ -235,7 +235,7 @@
"EVEN" > "HOL4Base.arithmetic.EVEN"
"EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
"EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel"
- "EQ_LESS_EQ" > "HOL.order_eq_iff"
+ "EQ_LESS_EQ" > "Orderings.order_eq_iff"
"EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
"EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel"
"DIV_UNIQUE" > "HOL4Base.arithmetic.DIV_UNIQUE"
--- a/src/HOL/Import/HOL/bool.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/bool.imp Fri Apr 01 18:59:17 2005 +0200
@@ -37,7 +37,7 @@
"bool_case_thm" > "HOL4Base.bool.bool_case_thm"
"bool_case_ID" > "HOL4Base.bool.bool_case_ID"
"bool_case_DEF" > "HOL4Compat.bool_case_DEF"
- "bool_INDUCT" > "Set.bool_induct"
+ "bool_INDUCT" > "Datatype.bool.induct"
"boolAxiom" > "HOL4Base.bool.boolAxiom"
"UNWIND_THM2" > "HOL.simp_thms_39"
"UNWIND_THM1" > "HOL.simp_thms_40"
@@ -78,7 +78,7 @@
"OR_INTRO_THM2" > "HOL.disjI2"
"OR_INTRO_THM1" > "HOL.disjI1"
"OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM"
- "OR_ELIM_THM" > "Recdef.tfl_disjE"
+ "OR_ELIM_THM" > "HOL.disjE"
"OR_DEF" > "HOL.or_def"
"OR_CONG" > "HOL4Base.bool.OR_CONG"
"OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
@@ -93,10 +93,10 @@
"NOT_DEF" > "HOL.simp_thms_19"
"NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES"
"NOT_AND" > "HOL4Base.bool.NOT_AND"
- "MONO_OR" > "Inductive.basic_monos_3"
+ "MONO_OR" > "Sum_Type.basic_monos_3"
"MONO_NOT" > "HOL.rev_contrapos"
"MONO_IMP" > "Set.imp_mono"
- "MONO_EXISTS" > "Inductive.basic_monos_5"
+ "MONO_EXISTS" > "Sum_Type.basic_monos_5"
"MONO_COND" > "HOL4Base.bool.MONO_COND"
"MONO_AND" > "Hilbert_Choice.conj_forward"
"MONO_ALL" > "Inductive.basic_monos_6"
@@ -139,12 +139,12 @@
"EXISTS_OR_THM" > "HOL.ex_disj_distrib"
"EXISTS_DEF" > "HOL4Setup.EXISTS_DEF"
"EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE"
- "ETA_THM" > "Presburger.fm_modd_pinf"
- "ETA_AX" > "Presburger.fm_modd_pinf"
+ "ETA_THM" > "HOL.eta_contract_eq"
+ "ETA_AX" > "HOL.eta_contract_eq"
"EQ_TRANS" > "Set.basic_trans_rules_31"
"EQ_SYM_EQ" > "HOL.eq_sym_conv"
"EQ_SYM" > "HOL.meta_eq_to_obj_eq"
- "EQ_REFL" > "Presburger.fm_modd_pinf"
+ "EQ_REFL" > "HOL.refl"
"EQ_IMP_THM" > "HOL.iff_conv_conj_imp"
"EQ_EXT" > "HOL.meta_eq_to_obj_eq"
"EQ_EXPAND" > "HOL4Base.bool.EQ_EXPAND"
@@ -152,7 +152,7 @@
"DISJ_SYM" > "HOL.disj_comms_1"
"DISJ_IMP_THM" > "HOL.imp_disjL"
"DISJ_COMM" > "HOL.disj_comms_1"
- "DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
+ "DISJ_ASSOC" > "HOL.disj_assoc"
"DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM"
"CONJ_SYM" > "HOL.conj_comms_1"
"CONJ_COMM" > "HOL.conj_comms_1"
@@ -172,8 +172,8 @@
"BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT"
"BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM"
"BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT"
- "BOOL_CASES_AX" > "HOL.True_or_False"
- "BETA_THM" > "Presburger.fm_modd_pinf"
+ "BOOL_CASES_AX" > "Datatype.bool.nchotomy"
+ "BETA_THM" > "HOL.eta_contract_eq"
"ARB_def" > "HOL4Base.bool.ARB_def"
"ARB_DEF" > "HOL4Base.bool.ARB_DEF"
"AND_INTRO_THM" > "HOL.conjI"
@@ -183,7 +183,7 @@
"AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES"
"AND2_THM" > "HOL.conjunct2"
"AND1_THM" > "HOL.conjunct1"
- "ABS_SIMP" > "Presburger.fm_modd_pinf"
+ "ABS_SIMP" > "HOL.refl"
"ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM"
ignore_thms
--- a/src/HOL/Import/HOL/num.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/num.imp Fri Apr 01 18:59:17 2005 +0200
@@ -12,7 +12,7 @@
thm_maps
"NOT_SUC" > "Nat.nat.simps_1"
"INV_SUC" > "Nat.Suc_inject"
- "INDUCTION" > "List.lexn.induct"
+ "INDUCTION" > "NatArith.of_nat.induct"
ignore_thms
"num_TY_DEF"
--- a/src/HOL/Import/HOL/pair.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/pair.imp Fri Apr 01 18:59:17 2005 +0200
@@ -21,7 +21,7 @@
"##" > "prod_fun"
thm_maps
- "pair_induction" > "Product_Type.prod_induct"
+ "pair_induction" > "Datatype.prod.induct"
"pair_case_thm" > "Product_Type.split"
"pair_case_def" > "HOL4Compat.pair_case_def"
"pair_case_cong" > "HOL4Base.pair.pair_case_cong"
@@ -41,7 +41,7 @@
"PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
"PAIR_MAP_THM" > "Product_Type.prod_fun"
"PAIR_MAP" > "HOL4Compat.PAIR_MAP"
- "PAIR_EQ" > "Product_Type.Pair_eq"
+ "PAIR_EQ" > "Datatype.prod.simps_1"
"PAIR" > "HOL4Compat.PAIR"
"LEX_def" > "HOL4Base.pair.LEX_def"
"LEX_DEF" > "HOL4Base.pair.LEX_DEF"
@@ -57,8 +57,8 @@
"CURRY_UNCURRY_THM" > "Product_Type.curry_split"
"CURRY_ONE_ONE_THM" > "HOL4Base.pair.CURRY_ONE_ONE_THM"
"CURRY_DEF" > "Product_Type.curry_conv"
- "CLOSED_PAIR_EQ" > "Product_Type.Pair_eq"
- "ABS_PAIR_THM" > "Product_Type.surj_pair"
+ "CLOSED_PAIR_EQ" > "Datatype.prod.simps_1"
+ "ABS_PAIR_THM" > "Datatype.prod.nchotomy"
ignore_thms
"prod_TY_DEF"
--- a/src/HOL/Import/HOL/prob_extra.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/prob_extra.imp Fri Apr 01 18:59:17 2005 +0200
@@ -39,7 +39,7 @@
"MEM_FILTER" > "HOL4Prob.prob_extra.MEM_FILTER"
"MAP_MEM" > "HOL4Prob.prob_extra.MAP_MEM"
"MAP_ID" > "List.map_ident"
- "LENGTH_FILTER" > "List.length_filter"
+ "LENGTH_FILTER" > "List.length_filter_le"
"LAST_MEM" > "HOL4Prob.prob_extra.LAST_MEM"
"LAST_MAP_CONS" > "HOL4Prob.prob_extra.LAST_MAP_CONS"
"IS_PREFIX_TRANS" > "HOL4Prob.prob_extra.IS_PREFIX_TRANS"
--- a/src/HOL/Import/HOL/real.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/real.imp Fri Apr 01 18:59:17 2005 +0200
@@ -28,7 +28,7 @@
"real_sub" > "OrderedGroup.diff_def"
"real_of_num" > "HOL4Compat.real_of_num"
"real_lte" > "HOL4Compat.real_lte"
- "real_lt" > "HOL.linorder_not_le"
+ "real_lt" > "Orderings.linorder_not_le"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
"real_div" > "Ring_and_Field.field.divide_inverse"
@@ -77,21 +77,21 @@
"REAL_SUB_RZERO" > "OrderedGroup.diff_0_right"
"REAL_SUB_RNEG" > "OrderedGroup.diff_minus_eq_add"
"REAL_SUB_REFL" > "OrderedGroup.diff_self"
- "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_6"
+ "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_3"
"REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2"
"REAL_SUB_LZERO" > "OrderedGroup.diff_0"
- "REAL_SUB_LT" > "RealDef.real_0_less_diff_iff"
+ "REAL_SUB_LT" > "HOL4Real.real.REAL_SUB_LT"
"REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG"
- "REAL_SUB_LE" > "RealDef.real_0_le_diff_iff"
- "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_7"
+ "REAL_SUB_LE" > "HOL4Real.real.REAL_SUB_LE"
+ "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
"REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2"
"REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2"
"REAL_SUB_ADD" > "OrderedGroup.diff_add_cancel"
"REAL_SUB_ABS" > "HOL4Real.real.REAL_SUB_ABS"
"REAL_SUB_0" > "OrderedGroup.eq_iff_diff_eq_0"
"REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
- "REAL_RINV_UNIQ" > "RealDef.real_inverse_unique"
- "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
+ "REAL_RINV_UNIQ" > "Ring_and_Field.inverse_unique"
+ "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_1"
"REAL_POW_POW" > "Power.power_mult"
"REAL_POW_MONO_LT" > "Power.power_strict_increasing"
"REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2"
@@ -112,7 +112,7 @@
"REAL_OF_NUM_ADD" > "RealDef.real_of_nat_add"
"REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT"
"REAL_NOT_LT" > "HOL4Compat.real_lte"
- "REAL_NOT_LE" > "HOL.linorder_not_le"
+ "REAL_NOT_LE" > "Orderings.linorder_not_le"
"REAL_NEG_SUB" > "OrderedGroup.minus_diff_eq"
"REAL_NEG_RMUL" > "Ring_and_Field.minus_mult_right"
"REAL_NEG_NEG" > "OrderedGroup.minus_minus"
@@ -129,7 +129,7 @@
"REAL_NEG_ADD" > "OrderedGroup.minus_add_distrib"
"REAL_NEG_0" > "OrderedGroup.minus_zero"
"REAL_NEGNEG" > "OrderedGroup.minus_minus"
- "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2"
+ "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_6"
"REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right"
"REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right"
"REAL_MUL_RINV" > "Ring_and_Field.right_inverse"
@@ -150,7 +150,7 @@
"REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict.mult_strict_right_mono"
"REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0"
"REAL_LT_RMUL" > "RealDef.real_mult_less_iff1"
- "REAL_LT_REFL" > "HOL.order_less_irrefl"
+ "REAL_LT_REFL" > "Orderings.order_less_irrefl"
"REAL_LT_RDIV_EQ" > "Ring_and_Field.pos_less_divide_eq"
"REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0"
"REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV"
@@ -164,17 +164,17 @@
"REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono"
"REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0"
"REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL"
- "REAL_LT_LE" > "HOL.order.order_less_le"
+ "REAL_LT_LE" > "Orderings.order.order_less_le"
"REAL_LT_LDIV_EQ" > "Ring_and_Field.pos_divide_less_eq"
"REAL_LT_LADD" > "OrderedGroup.add_less_cancel_left"
"REAL_LT_INV_EQ" > "Ring_and_Field.inverse_positive_iff_positive"
"REAL_LT_INV" > "Ring_and_Field.less_imp_inverse_less"
- "REAL_LT_IMP_NE" > "HOL.less_imp_neq"
- "REAL_LT_IMP_LE" > "HOL.order_less_imp_le"
+ "REAL_LT_IMP_NE" > "Orderings.less_imp_neq"
+ "REAL_LT_IMP_LE" > "Orderings.order_less_imp_le"
"REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
"REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2"
"REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff"
- "REAL_LT_GT" > "HOL.order_less_not_sym"
+ "REAL_LT_GT" > "Orderings.order_less_not_sym"
"REAL_LT_FRACTION_0" > "HOL4Real.real.REAL_LT_FRACTION_0"
"REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION"
"REAL_LT_DIV" > "HOL4Real.real.REAL_LT_DIV"
@@ -199,18 +199,18 @@
"REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ"
"REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ"
"REAL_LE_TRANS" > "Set.basic_trans_rules_25"
- "REAL_LE_TOTAL" > "HOL.linorder.linorder_linear"
+ "REAL_LE_TOTAL" > "Orderings.linorder.linorder_linear"
"REAL_LE_SUB_RADD" > "OrderedGroup.compare_rls_8"
"REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9"
"REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square"
"REAL_LE_RNEG" > "OrderedGroup.le_eq_neg"
"REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring.mult_right_mono"
"REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1"
- "REAL_LE_REFL" > "HOL.order.order_refl"
+ "REAL_LE_REFL" > "Orderings.order.order_refl"
"REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq"
"REAL_LE_RDIV" > "HOL4Real.real.REAL_LE_RDIV"
"REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right"
- "REAL_LE_POW2" > "NatBin.zero_le_power2"
+ "REAL_LE_POW2" > "NatBin.zero_compare_simps_12"
"REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
"REAL_LE_NEGR" > "OrderedGroup.le_minus_self_iff"
"REAL_LE_NEGL" > "OrderedGroup.minus_le_self_iff"
@@ -218,7 +218,7 @@
"REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le"
"REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2"
"REAL_LE_MUL" > "Ring_and_Field.mult_pos_le"
- "REAL_LE_LT" > "HOL.order_le_less"
+ "REAL_LE_LT" > "Orderings.order_le_less"
"REAL_LE_LNEG" > "RealDef.real_0_le_add_iff"
"REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono"
"REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2"
@@ -230,20 +230,20 @@
"REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV"
"REAL_LE_DOUBLE" > "OrderedGroup.zero_le_double_add_iff_zero_le_single_add"
"REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV"
- "REAL_LE_ANTISYM" > "HOL.order_eq_iff"
+ "REAL_LE_ANTISYM" > "Orderings.order_eq_iff"
"REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR"
"REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL"
"REAL_LE_ADD2" > "OrderedGroup.add_mono"
"REAL_LE_ADD" > "RealDef.real_le_add_order"
"REAL_LE_01" > "Ring_and_Field.zero_le_one"
"REAL_LET_TRANS" > "Set.basic_trans_rules_23"
- "REAL_LET_TOTAL" > "HOL4Real.real.REAL_LET_TOTAL"
+ "REAL_LET_TOTAL" > "Orderings.linorder_le_less_linear"
"REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM"
"REAL_LET_ADD2" > "OrderedGroup.add_le_less_mono"
"REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD"
"REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
"REAL_LE" > "RealDef.real_of_nat_le_iff"
- "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
+ "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
"REAL_INV_POS" > "Ring_and_Field.positive_imp_inverse_positive"
"REAL_INV_NZ" > "Ring_and_Field.nonzero_imp_inverse_nonzero"
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
@@ -270,7 +270,7 @@
"REAL_EQ_LMUL" > "Ring_and_Field.field_mult_cancel_left"
"REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ"
"REAL_EQ_LADD" > "OrderedGroup.add_left_cancel"
- "REAL_EQ_IMP_LE" > "HOL.order_eq_refl"
+ "REAL_EQ_IMP_LE" > "Orderings.order_eq_refl"
"REAL_ENTIRE" > "Ring_and_Field.field_mult_eq_0_iff"
"REAL_DOWN2" > "RealDef.real_lbound_gt_zero"
"REAL_DOWN" > "HOL4Real.real.REAL_DOWN"
@@ -289,11 +289,11 @@
"REAL_ADD_RINV" > "OrderedGroup.right_minus"
"REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
"REAL_ADD_RID" > "OrderedGroup.add_0_right"
- "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
+ "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_1"
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
"REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ"
"REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0"
- "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
+ "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
"REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
"REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2"
"REAL_ADD" > "RealDef.real_of_nat_add"
@@ -330,7 +330,7 @@
"ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
"ABS_SUM" > "HOL4Real.real.ABS_SUM"
"ABS_SUB_ABS" > "HOL4Real.real.ABS_SUB_ABS"
- "ABS_SUB" > "HOL4Real.real.ABS_SUB"
+ "ABS_SUB" > "OrderedGroup.abs_minus_commute"
"ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ"
"ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
"ABS_SIGN" > "HOL4Real.real.ABS_SIGN"
--- a/src/HOL/Import/HOL/realax.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/realax.imp Fri Apr 01 18:59:17 2005 +0200
@@ -91,16 +91,16 @@
"TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC"
"TREAL_10" > "HOL4Real.realax.TREAL_10"
"REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
- "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2"
+ "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_6"
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
"REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1"
"REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
"REAL_LT_TRANS" > "Set.basic_trans_rules_21"
"REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
- "REAL_LT_REFL" > "HOL.order_less_irrefl"
+ "REAL_LT_REFL" > "Orderings.order_less_irrefl"
"REAL_LT_MUL" > "Ring_and_Field.mult_pos"
"REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
- "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
+ "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
"REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"
"REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
--- a/src/HOL/Import/HOL/rich_list.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/rich_list.imp Fri Apr 01 18:59:17 2005 +0200
@@ -253,7 +253,7 @@
"FIRSTN_APPEND1" > "HOL4Base.rich_list.FIRSTN_APPEND1"
"FIRSTN" > "HOL4Base.rich_list.FIRSTN"
"FILTER_SNOC" > "HOL4Base.rich_list.FILTER_SNOC"
- "FILTER_REVERSE" > "HOL4Base.rich_list.FILTER_REVERSE"
+ "FILTER_REVERSE" > "List.rev_filter"
"FILTER_MAP" > "HOL4Base.rich_list.FILTER_MAP"
"FILTER_IDEM" > "HOL4Base.rich_list.FILTER_IDEM"
"FILTER_FOLDR" > "HOL4Base.rich_list.FILTER_FOLDR"
@@ -357,7 +357,7 @@
"AND_EL_DEF" > "HOL4Base.rich_list.AND_EL_DEF"
"ALL_EL_SNOC" > "HOL4Base.rich_list.ALL_EL_SNOC"
"ALL_EL_SEG" > "HOL4Base.rich_list.ALL_EL_SEG"
- "ALL_EL_REVERSE" > "HOL4Base.rich_list.ALL_EL_REVERSE"
+ "ALL_EL_REVERSE" > "List.list_all_rev"
"ALL_EL_REPLICATE" > "HOL4Base.rich_list.ALL_EL_REPLICATE"
"ALL_EL_MAP" > "HOL4Base.rich_list.ALL_EL_MAP"
"ALL_EL_LASTN" > "HOL4Base.rich_list.ALL_EL_LASTN"
--- a/src/HOL/Import/HOL/sum.imp Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/sum.imp Fri Apr 01 18:59:17 2005 +0200
@@ -11,12 +11,12 @@
"OUTL" > "HOL4Compat.OUTL"
"ISR" > "HOL4Compat.ISR"
"ISL" > "HOL4Compat.ISL"
- "INR" > "Inr"
- "INL" > "Inl"
+ "INR" > "Sum_Type.Inr"
+ "INL" > "Sum_Type.Inl"
thm_maps
- "sum_distinct1" > "Sum_Type.Inr_not_Inl"
- "sum_distinct" > "Sum_Type.Inl_not_Inr"
+ "sum_distinct1" > "Datatype.sum.simps_2"
+ "sum_distinct" > "Datatype.sum.simps_1"
"sum_case_def" > "HOL4Compat.sum_case_def"
"sum_case_cong" > "HOL4Base.sum.sum_case_cong"
"sum_INDUCT" > "HOL4Compat.OUTR.induct"
@@ -26,7 +26,7 @@
"ISR" > "HOL4Compat.ISR"
"ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR"
"ISL" > "HOL4Compat.ISL"
- "INR_neq_INL" > "Sum_Type.Inr_not_Inl"
+ "INR_neq_INL" > "Datatype.sum.simps_2"
"INR_INL_11" > "HOL4Compat.INR_INL_11"
"INR" > "HOL4Base.sum.INR"
"INL" > "HOL4Base.sum.INL"
--- a/src/HOL/Import/hol4rews.ML Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/hol4rews.ML Fri Apr 01 18:59:17 2005 +0200
@@ -496,7 +496,7 @@
end;
fun setup_dump (dir,thyname) thy =
- HOL4Dump.put (dir,thyname,[]) thy
+ HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
fun add_dump str thy =
let
--- a/src/HOL/Import/proof_kernel.ML Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Apr 01 18:59:17 2005 +0200
@@ -203,7 +203,7 @@
then F true n
else F false (n+1)
in
- transform_error (Library.setmp Syntax.ambiguity_is_error true (F false)) 0
+ transform_error (Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true (F false))) 0
end
handle ERROR_MESSAGE mesg =>
(writeln "Exception in smart_string_of_cterm!";
@@ -1217,6 +1217,7 @@
fun get_isabelle_thm thyname thmname hol4conc thy =
let
+ val _ = message "get_isabelle_thm called..."
val sg = sign_of thy
val (info,hol4conc') = disamb_term hol4conc
@@ -1257,7 +1258,7 @@
if_debug prin isaconc)
val cs = non_trivial_term_consts isaconc
val _ = (message "Looking for consts:";
- message (String.concat cs))
+ message (commas cs))
val pot_thms = Shuffler.find_potential thy isaconc
val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
in
@@ -1273,16 +1274,16 @@
| NONE => (thy,NONE)
end
end
- handle _ => (thy,NONE)
+ handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE))
fun get_thm thyname thmname thy =
case get_hol4_thm thyname thmname thy of
SOME hth => (thy,SOME hth)
| NONE => ((case fst (import_proof thyname thmname thy) of
SOME f => get_isabelle_thm thyname thmname (f thy) thy
- | NONE => (thy,NONE))
- handle e as IO.Io _ => (thy,NONE)
- | e as PK _ => (thy,NONE))
+ | NONE => (message "No conclusion"; (thy,NONE)))
+ handle e as IO.Io _ => (message "IO exception"; (thy,NONE))
+ | e as PK _ => (message "PK exception"; (thy,NONE)))
fun rename_const thyname thy name =
case get_hol4_const_renaming thyname name thy of
--- a/src/HOL/IsaMakefile Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 01 18:59:17 2005 +0200
@@ -6,7 +6,7 @@
default: HOL
generate: HOL-Complex-Generate-HOL
-images: HOL HOL-Algebra HOL-Complex TLA ####lcp temporary####HOL4
+images: HOL HOL-Algebra HOL-Complex TLA HOL4
#Note: keep targets sorted (except for HOL-Library)
test: \