--- a/src/HOL/HOL.thy Fri Oct 06 14:43:26 1995 +0100
+++ b/src/HOL/HOL.thy Fri Oct 06 16:17:08 1995 +0100
@@ -142,9 +142,11 @@
o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
end
-
ML
(** Choice between the HOL and Isabelle style of quantifiers **)
@@ -163,3 +165,9 @@
val print_ast_translation =
map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
+
+(* start 8bit 2 *)
+(* end 8bit 2 *)
+
+
+
--- a/src/HOL/Prod.thy Fri Oct 06 14:43:26 1995 +0100
+++ b/src/HOL/Prod.thy Fri Oct 06 16:17:08 1995 +0100
@@ -74,6 +74,9 @@
defs
Unity_def "() == Abs_Unit(True)"
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
end
(*
ML
--- a/src/HOL/ROOT.ML Fri Oct 06 14:43:26 1995 +0100
+++ b/src/HOL/ROOT.ML Fri Oct 06 16:17:08 1995 +0100
@@ -61,6 +61,7 @@
addSEs [exE,ex1E] addEs [allE];
use "simpdata.ML";
+
use_thy "Ord";
use_thy "subset";
use "hologic.ML";
--- a/src/HOL/Set.thy Fri Oct 06 14:43:26 1995 +0100
+++ b/src/HOL/Set.thy Fri Oct 06 16:17:08 1995 +0100
@@ -100,6 +100,9 @@
inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
surj_def "surj(f) == ! y. ? x. y=f(x)"
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
end
ML