added 8bit pragmas
authorregensbu
Fri Oct 06 16:17:08 1995 +0100 (1995-10-06)
changeset 12736960ec882bca
parent 1272 dd877dc7c1f4
child 1274 ea0668a1c0ba
added 8bit pragmas
src/HOL/HOL.thy
src/HOL/Prod.thy
src/HOL/ROOT.ML
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Fri Oct 06 14:43:26 1995 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Oct 06 16:17:08 1995 +0100
     1.3 @@ -142,9 +142,11 @@
     1.4    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
     1.5    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
     1.6  
     1.7 +(* start 8bit 1 *)
     1.8 +(* end 8bit 1 *)
     1.9 +
    1.10  end
    1.11  
    1.12 -
    1.13  ML
    1.14  
    1.15  (** Choice between the HOL and Isabelle style of quantifiers **)
    1.16 @@ -163,3 +165,9 @@
    1.17  
    1.18  val print_ast_translation =
    1.19    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    1.20 +
    1.21 +(* start 8bit 2 *)
    1.22 +(* end 8bit 2 *)
    1.23 +
    1.24 +
    1.25 +
     2.1 --- a/src/HOL/Prod.thy	Fri Oct 06 14:43:26 1995 +0100
     2.2 +++ b/src/HOL/Prod.thy	Fri Oct 06 16:17:08 1995 +0100
     2.3 @@ -74,6 +74,9 @@
     2.4  defs
     2.5    Unity_def     "() == Abs_Unit(True)"
     2.6  
     2.7 +(* start 8bit 1 *)
     2.8 +(* end 8bit 1 *)
     2.9 +
    2.10  end
    2.11  (*
    2.12  ML
     3.1 --- a/src/HOL/ROOT.ML	Fri Oct 06 14:43:26 1995 +0100
     3.2 +++ b/src/HOL/ROOT.ML	Fri Oct 06 16:17:08 1995 +0100
     3.3 @@ -61,6 +61,7 @@
     3.4                       addSEs [exE,ex1E] addEs [allE];
     3.5  
     3.6  use     "simpdata.ML";
     3.7 +
     3.8  use_thy "Ord";
     3.9  use_thy "subset";
    3.10  use     "hologic.ML";
     4.1 --- a/src/HOL/Set.thy	Fri Oct 06 14:43:26 1995 +0100
     4.2 +++ b/src/HOL/Set.thy	Fri Oct 06 16:17:08 1995 +0100
     4.3 @@ -100,6 +100,9 @@
     4.4    inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     4.5    surj_def      "surj(f)        == ! y. ? x. y=f(x)"
     4.6  
     4.7 +(* start 8bit 1 *)
     4.8 +(* end 8bit 1 *)
     4.9 +
    4.10  end
    4.11  
    4.12  ML