src/Pure/axclass.ML
changeset 32765 3032c0308019
parent 32197 bc341bbe4417
child 32791 e6d47ce70d27
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
   417       |> n = 0 ? Thm.eq_assumption 1;
   417       |> n = 0 ? Thm.eq_assumption 1;
   418     val dests =
   418     val dests =
   419       if n = 0 then []
   419       if n = 0 then []
   420       else
   420       else
   421         (eq RS Drule.equal_elim_rule1)
   421         (eq RS Drule.equal_elim_rule1)
   422         |> BalancedTree.dest (fn th =>
   422         |> Balanced_Tree.dest (fn th =>
   423           (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n;
   423           (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n;
   424   in (intro, dests) end;
   424   in (intro, dests) end;
   425 
   425 
   426 fun define_class (bclass, raw_super) raw_params raw_specs thy =
   426 fun define_class (bclass, raw_super) raw_params raw_specs thy =
   427   let
   427   let