# HG changeset patch
# User regensbu
# Date 812992628 -3600
# Node ID 6960ec882bca8146fca07b26dde551b66ca9105b
# Parent  dd877dc7c1f4fddb9201633cf80103f14510574b
added 8bit pragmas

diff -r dd877dc7c1f4 -r 6960ec882bca src/HOL/HOL.thy
--- 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 *)
+
+
+
diff -r dd877dc7c1f4 -r 6960ec882bca src/HOL/Prod.thy
--- 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
diff -r dd877dc7c1f4 -r 6960ec882bca src/HOL/ROOT.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";
diff -r dd877dc7c1f4 -r 6960ec882bca src/HOL/Set.thy
--- 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