comment
authorwenzelm
Thu Feb 01 20:45:11 2001 +0100 (2001-02-01)
changeset 1102141de937d338b
parent 11020 646c929b6293
child 11022 72a76580ed2f
comment
src/Pure/Isar/obtain.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Feb 01 20:44:19 2001 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Feb 01 20:45:11 2001 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5    {
     1.6      fix thesis
     1.7 -    assume that: "!!x. P x ==> thesis"
     1.8 +    assume that [intro]: "!!x. P x ==> thesis"
     1.9      <chain_facts> have thesis <proof (insert that)>
    1.10    }
    1.11    fix x assm (obtained) "P x"
     2.1 --- a/src/Pure/library.ML	Thu Feb 01 20:44:19 2001 +0100
     2.2 +++ b/src/Pure/library.ML	Thu Feb 01 20:45:11 2001 +0100
     2.3 @@ -271,7 +271,7 @@
     2.4    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
     2.5    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
     2.6    val transitive_closure: (string * string list) list -> (string * string list) list
     2.7 -  val init_gensym: unit -> unit
     2.8 +  val init_gensym: unit -> unit    (* FIXME !!??! *)
     2.9    val gensym: string -> string
    2.10    val bump_int_list: string list -> string list
    2.11    val bump_list: string list * string -> string list
    2.12 @@ -1344,7 +1344,7 @@
    2.13  
    2.14  in
    2.15  
    2.16 -fun init_gensym() = (seedr := 0);
    2.17 +fun init_gensym() = (seedr := 0);    (* FIXME !!??! *)
    2.18  
    2.19  fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr));
    2.20  end;