src/Pure/conjunction.ML
changeset 32765 3032c0308019
parent 30823 eb99b9134f2e
child 33277 1bdc3c732fdd
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
    36 val conjunction = certify Logic.conjunction;
    36 val conjunction = certify Logic.conjunction;
    37 
    37 
    38 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    38 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    39 
    39 
    40 fun mk_conjunction_balanced [] = true_prop
    40 fun mk_conjunction_balanced [] = true_prop
    41   | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
    41   | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
    42 
    42 
    43 fun dest_conjunction ct =
    43 fun dest_conjunction ct =
    44   (case Thm.term_of ct of
    44   (case Thm.term_of ct of
    45     (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    45     (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    46   | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
    46   | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
   115 
   115 
   116 
   116 
   117 (* balanced conjuncts *)
   117 (* balanced conjuncts *)
   118 
   118 
   119 fun intr_balanced [] = asm_rl
   119 fun intr_balanced [] = asm_rl
   120   | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
   120   | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;
   121 
   121 
   122 fun elim_balanced 0 _ = []
   122 fun elim_balanced 0 _ = []
   123   | elim_balanced n th = BalancedTree.dest elim n th;
   123   | elim_balanced n th = Balanced_Tree.dest elim n th;
   124 
   124 
   125 
   125 
   126 (* currying *)
   126 (* currying *)
   127 
   127 
   128 local
   128 local