2 sig

     2 sig

     3   exception LIFT_MATCH of string

     3   exception LIFT_MATCH of string

     4 

     4 

     5   val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state

     5   val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state

     6   val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state

     6   val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state

     7 

     7 

     8 end;

     8 end;

     9 

     9 

    11 struct

    11 struct

    12 

    14 

    13 exception LIFT_MATCH of string

    15 exception LIFT_MATCH of string

    14 

    16 

    15 (* wrappers for define, note, Attrib.internal and theorem_i *)

    17 (* wrappers for define, note, Attrib.internal and theorem_i *)

    16 fun define (name, mx, rhs) lthy =

    18 fun define (name, mx, rhs) lthy =

   221       "quotient type definitions (requires equivalence proofs)"

   223       "quotient type definitions (requires equivalence proofs)"

   222          OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)

   224          OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)

   223 

   225 

   224 end; (* structure *)

   226 end; (* structure *)

   225 

   227