src/ZF/Datatype_ZF.thy
changeset 32765 3032c0308019
parent 32740 9dd0a2f83429
child 35409 5c5bb83f2bae
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
    61 struct
    61 struct
    62   val trace = Unsynchronized.ref false;
    62   val trace = Unsynchronized.ref false;
    63 
    63 
    64   fun mk_new ([],[]) = Const("True",FOLogic.oT)
    64   fun mk_new ([],[]) = Const("True",FOLogic.oT)
    65     | mk_new (largs,rargs) =
    65     | mk_new (largs,rargs) =
    66         BalancedTree.make FOLogic.mk_conj
    66         Balanced_Tree.make FOLogic.mk_conj
    67                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    67                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    68 
    68 
    69  val datatype_ss = @{simpset};
    69  val datatype_ss = @{simpset};
    70 
    70 
    71  fun proc sg ss old =
    71  fun proc sg ss old =