src/HOL/List.ML
changeset 14401 477380c74c1d
parent 14025 d9b155757dc8
child 15246 0984a2c2868b
     1.1 --- a/src/HOL/List.ML	Thu Feb 19 17:57:54 2004 +0100
     1.2 +++ b/src/HOL/List.ML	Thu Feb 19 18:24:08 2004 +0100
     1.3 @@ -1,40 +1,6 @@
     1.4  
     1.5  (** legacy ML bindings **)
     1.6  
     1.7 -structure List =
     1.8 -struct
     1.9 -
    1.10 -val thy = the_context ();
    1.11 -
    1.12 -structure list =
    1.13 -struct
    1.14 -  val distinct = thms "list.distinct";
    1.15 -  val inject = thms "list.inject";
    1.16 -  val exhaust = thm "list.exhaust";
    1.17 -  val cases = thms "list.cases";
    1.18 -  val split = thm "list.split";
    1.19 -  val split_asm = thm "list.split_asm";
    1.20 -  val induct = thm "list.induct";
    1.21 -  val recs = thms "list.recs";
    1.22 -  val simps = thms "list.simps";
    1.23 -  val size = thms "list.size";
    1.24 -end;
    1.25 -
    1.26 -structure lists =
    1.27 -struct
    1.28 -  val intrs = thms "lists.intros";
    1.29 -  val elims = thms "lists.cases";
    1.30 -  val elim = thm "lists.cases";
    1.31 -  val induct = thm "lists.induct";
    1.32 -  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "List.lists";
    1.33 -  val [Nil, Cons] = intrs;
    1.34 -end;
    1.35 -
    1.36 -end;
    1.37 -
    1.38 -open List;
    1.39 -
    1.40 -
    1.41  val Cons_eq_appendI = thm "Cons_eq_appendI";
    1.42  val Cons_in_lex = thm "Cons_in_lex";
    1.43  val Nil2_notin_lex = thm "Nil2_notin_lex";