tuned;
authorwenzelm
Fri Mar 01 22:28:59 2002 +0100 (2002-03-01)
changeset 129998ad8d02b973f
parent 12998 03b9afa801df
child 13000 e56aedec11f3
tuned;
ANNOUNCE
src/HOL/HOL.ML
     1.1 --- a/ANNOUNCE	Fri Mar 01 18:12:16 2002 +0100
     1.2 +++ b/ANNOUNCE	Fri Mar 01 22:28:59 2002 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5    * HOL/HoareParallel: large application concerning verification of
     1.6      parallel imperative programs (Owicki-Gries method, Rely-Guarantee
     1.7 -    method, verification examples: garbage collection, mutual
     1.8 +    method, including examples of garbage collection, mutual
     1.9      exclusion, etc.)
    1.10      (by Leonor Prensa Nieto).
    1.11  
     2.1 --- a/src/HOL/HOL.ML	Fri Mar 01 18:12:16 2002 +0100
     2.2 +++ b/src/HOL/HOL.ML	Fri Mar 01 22:28:59 2002 +0100
     2.3 @@ -1,35 +1,5 @@
     2.4 -(*  Title:      HOL/HOL.ML
     2.5 -    ID:         $Id$
     2.6 -*)
     2.7  
     2.8 -structure HOL =
     2.9 -struct
    2.10 -  val thy = the_context ();
    2.11 -  val plusI = plusI;
    2.12 -  val minusI = minusI;
    2.13 -  val timesI = timesI;
    2.14 -  val eq_reflection = eq_reflection;
    2.15 -  val refl = refl;
    2.16 -  val subst = subst;
    2.17 -  val ext = ext;
    2.18 -  val impI = impI;
    2.19 -  val mp = mp;
    2.20 -  val True_def = True_def;
    2.21 -  val All_def = All_def;
    2.22 -  val Ex_def = Ex_def;
    2.23 -  val False_def = False_def;
    2.24 -  val not_def = not_def;
    2.25 -  val and_def = and_def;
    2.26 -  val or_def = or_def;
    2.27 -  val Ex1_def = Ex1_def;
    2.28 -  val iff = iff;
    2.29 -  val True_or_False = True_or_False;
    2.30 -  val Let_def = Let_def;
    2.31 -  val if_def = if_def;
    2.32 -  val arbitrary_def = arbitrary_def;
    2.33 -end;
    2.34 -
    2.35 -open HOL;
    2.36 +(* legacy ML bindings *)
    2.37  
    2.38  val Least_def = thm "Least_def";
    2.39  val Least_equality = thm "Least_equality";
    2.40 @@ -83,3 +53,32 @@
    2.41  val order_antisym = thm "order_antisym";
    2.42  val order_less_le = thm "order_less_le";
    2.43  val linorder_linear = thm "linorder_linear";
    2.44 +
    2.45 +structure HOL =
    2.46 +struct
    2.47 +  val thy = the_context ();
    2.48 +  val plusI = plusI;
    2.49 +  val minusI = minusI;
    2.50 +  val timesI = timesI;
    2.51 +  val eq_reflection = eq_reflection;
    2.52 +  val refl = refl;
    2.53 +  val subst = subst;
    2.54 +  val ext = ext;
    2.55 +  val impI = impI;
    2.56 +  val mp = mp;
    2.57 +  val True_def = True_def;
    2.58 +  val All_def = All_def;
    2.59 +  val Ex_def = Ex_def;
    2.60 +  val False_def = False_def;
    2.61 +  val not_def = not_def;
    2.62 +  val and_def = and_def;
    2.63 +  val or_def = or_def;
    2.64 +  val Ex1_def = Ex1_def;
    2.65 +  val iff = iff;
    2.66 +  val True_or_False = True_or_False;
    2.67 +  val Let_def = Let_def;
    2.68 +  val if_def = if_def;
    2.69 +  val arbitrary_def = arbitrary_def;
    2.70 +end;
    2.71 +
    2.72 +open HOL;