--- a/src/HOL/Integ/Integ.ML Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/Integ/Integ.ML Tue Jan 30 15:24:36 1996 +0100
@@ -1,7 +1,7 @@
-(* Title: Integ.ML
+(* Title: Integ.ML
ID: $Id$
- Authors: Riccardo Mattolini, Dip. Sistemi e Informatica
- Lawrence C Paulson, Cambridge University Computer Laboratory
+ Authors: Riccardo Mattolini, Dip. Sistemi e Informatica
+ Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 Universita' di Firenze
Copyright 1993 University of Cambridge
@@ -84,7 +84,7 @@
qed "inj_onto_Abs_Integ";
Addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff,
- intrel_iff, intrel_in_integ, Abs_Integ_inverse];
+ intrel_iff, intrel_in_integ, Abs_Integ_inverse];
goal Integ.thy "inj(Rep_Integ)";
by (rtac inj_inverseI 1);
@@ -213,8 +213,8 @@
by (asm_simp_tac (!simpset addsimps [diff_add_inverse,diff_add_0]) 1);
by (rtac impI 1);
by (asm_simp_tac (!simpset addsimps
- [diff_add_inverse, diff_add_0, diff_Suc_add_0,
- diff_Suc_add_inverse]) 1);
+ [diff_add_inverse, diff_add_0, diff_Suc_add_0,
+ diff_Suc_add_inverse]) 1);
qed "zmagnitude_congruent";
(*Resolve th against the corresponding facts for zmagnitude*)
@@ -328,8 +328,8 @@
qed "zmult_congruent_lemma";
goal Integ.thy
- "congruent2 intrel (%p1 p2. \
-\ split (%x1 y1. split (%x2 y2. \
+ "congruent2 intrel (%p1 p2. \
+\ split (%x1 y1. split (%x2 y2. \
\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
by (safe_tac intrel_cs);
@@ -351,7 +351,7 @@
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
goalw Integ.thy [zmult_def]
- "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \
+ "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \
\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
by (simp_tac (!simpset addsimps [zmult_ize UN_equiv_class2]) 1);
qed "zmult";
@@ -433,7 +433,7 @@
val zminus_simps = [zminus_zminus, zminus_0, zminus_zadd_distrib];
val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right,
- zmult_zminus, zmult_zminus_right];
+ zmult_zminus, zmult_zminus_right];
Addsimps (zadd_simps @ zminus_simps @ zmult_simps @
[zmagnitude_znat, zmagnitude_zminus_znat]);
@@ -700,12 +700,12 @@
goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
- rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]);
+ rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]);
qed "zle_trans";
goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
- fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]);
+ fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]);
qed "zle_anti_sym";