src/ZF/Fin.ML
changeset 444 3ca9d49fd662
parent 437 435875e4b21d
child 477 53fc8ad84b33
     1.1 --- a/src/ZF/Fin.ML	Wed Jun 29 12:13:03 1994 +0200
     1.2 +++ b/src/ZF/Fin.ML	Fri Jul 01 11:03:42 1994 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  *)
     1.5  
     1.6  structure Fin = Inductive_Fun
     1.7 - (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]
     1.8 + (val thy        = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)]
     1.9    val rec_doms   = [("Fin","Pow(A)")]
    1.10    val sintrs     = ["0 : Fin(A)",
    1.11                      "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]