Main now new-style theory; added Main.ML for compatibility;
authorwenzelm
Fri Aug 18 17:53:49 2000 +0200 (2000-08-18)
changeset 96506f0b89f2a1f9
parent 9649 89155e48fa53
child 9651 f0cfddda6038
Main now new-style theory; added Main.ML for compatibility;
src/HOL/IsaMakefile
src/HOL/Main.ML
src/HOL/Main.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Aug 18 12:34:48 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Aug 18 17:53:49 2000 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4    Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML	\
     1.5    Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML		\
     1.6    Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML         \
     1.7 -  Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML        \
     1.8 +  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
     1.9    Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML  \
    1.10    Ord.thy Power.ML Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML       \
    1.11    Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML Relation.thy   \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Main.ML	Fri Aug 18 17:53:49 2000 +0200
     2.3 @@ -0,0 +1,5 @@
     2.4 +
     2.5 +structure Main =
     2.6 +struct
     2.7 +  val thy = the_context ();
     2.8 +end;
     3.1 --- a/src/HOL/Main.thy	Fri Aug 18 12:34:48 2000 +0200
     3.2 +++ b/src/HOL/Main.thy	Fri Aug 18 17:53:49 2000 +0200
     3.3 @@ -2,4 +2,7 @@
     3.4  (*theory Main includes everything; note that theory
     3.5    PreList already includes most HOL theories*)
     3.6  
     3.7 -Main = Map + String
     3.8 +theory Main = Map + String:
     3.9 +
    3.10 +end
    3.11 +