proper import of Main HOL;

--- a/src/HOL/Induct/LList.thy	Sat Sep 30 21:39:24 2006 +0200
+++ b/src/HOL/Induct/LList.thy	Sat Sep 30 21:39:25 2006 +0200
@@ -22,7 +22,7 @@
 
 header {*Definition of type llist by a greatest fixed point*}
 
-theory LList imports Main SList begin
+theory LList imports SList begin
 
 consts
 

--- a/src/HOL/Induct/SList.thy	Sat Sep 30 21:39:24 2006 +0200
+++ b/src/HOL/Induct/SList.thy	Sat Sep 30 21:39:25 2006 +0200
@@ -24,7 +24,7 @@
 Tidied by lcp.  Still needs removal of nat_rec.
 *)
 
-theory SList imports NatArith Sexp Hilbert_Choice begin
+theory SList imports Sexp begin
 
 (*Hilbert_Choice is needed for the function "inv"*)
 
@@ -38,10 +38,10 @@
 (* Defining the Concrete Constructors *)
 definition
   NIL  :: "'a item"
-   "NIL = In0(Numb(0))"
+  "NIL = In0(Numb(0))"
 
   CONS :: "['a item, 'a item] => 'a item"
-   "CONS M N = In1(Scons M N)"
+  "CONS M N = In1(Scons M N)"
 
 consts
   list      :: "'a item set => 'a item set"
@@ -52,16 +52,20 @@
 
 
 typedef (List)
-  'a list = "list(range Leaf) :: 'a item set" 
+    'a list = "list(range Leaf) :: 'a item set" 
   by (blast intro: list.NIL_I)
 
+abbreviation
+  "Case == Datatype_Universe.Case"
+  "Split == Datatype_Universe.Split"
+
 definition
   List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
-   "List_case c d = Case(%x. c)(Split(d))"
+  "List_case c d = Case(%x. c)(Split(d))"
   
   List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
-   "List_rec M c d = wfrec (trancl pred_sexp)
-                            (%g. List_case c (%x y. d x y (g y))) M"
+  "List_rec M c d = wfrec (trancl pred_sexp)
+                           (%g. List_case c (%x y. d x y (g y))) M"
 
 
 (* *********************************************************************** *)
@@ -72,6 +76,13 @@
 
 (*Declaring the abstract list constructors*)
 
+no_translations
+  "[x, xs]" == "x#[xs]"
+  "[x]" == "x#[]"
+no_syntax
+  Nil :: "'a list"  ("[]")
+  Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "#" 65)
+
 definition
   Nil       :: "'a list"                               ("[]")
    "Nil  = Abs_List(NIL)"
@@ -88,9 +99,6 @@
    "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
 
 (* list Enumeration *)
-syntax
-  "@list"   :: "args => 'a list"                    ("[(_)]")
-
 translations
   "[x, xs]" == "x#[xs]"
   "[x]"     == "x#[]"
@@ -196,10 +204,14 @@
   enum_Suc: "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"
 
 
+no_syntax
+  "@" :: "'a list => 'a list => 'a list"    (infixr 65)
+no_translations
+  "[x:xs . P]" == "filter (%x. P) xs"
+
 syntax
   (* Special syntax for list_all and filter *)
   "@Alls"       :: "[idt, 'a list, bool] => bool"        ("(2Alls _:_./ _)" 10)
-  "@filter"     :: "[idt, 'a list, bool] => 'a list"     ("(1[_:_ ./ _])")
 
 translations
   "[x:xs. P]" == "CONST filter(%x. P) xs"

--- a/src/HOL/Induct/Sexp.thy	Sat Sep 30 21:39:24 2006 +0200
+++ b/src/HOL/Induct/Sexp.thy	Sat Sep 30 21:39:25 2006 +0200
@@ -7,7 +7,14 @@
 structures by hand.
 *)
 
-theory Sexp imports Datatype_Universe Inductive begin
+theory Sexp imports Main begin
+
+types
+  'a item = "'a Datatype_Universe.item"
+abbreviation
+  "Leaf == Datatype_Universe.Leaf"
+  "Numb == Datatype_Universe.Numb"
+
 consts
   sexp      :: "'a item set"
 
@@ -18,12 +25,11 @@
     SconsI: "[| M \<in> sexp;  N \<in> sexp |] ==> Scons M N \<in> sexp"
 
 definition
-
   sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
                 'a item] => 'b"
-   "sexp_case c d e M = (THE z. (EX x.   M=Leaf(x) & z=c(x))  
-                            | (EX k.   M=Numb(k) & z=d(k))  
-                            | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2))"
+  "sexp_case c d e M = (THE z. (EX x.   M=Leaf(x) & z=c(x))  
+                             | (EX k.   M=Numb(k) & z=d(k))  
+                             | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2))"
 
   pred_sexp :: "('a item * 'a item)set"
      "pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})"