# HG changeset patch # User Christian Urban # Date 1256651198 -3600 # Node ID 2a803a1556d54838da43961b28e3025995fde75c # Parent 524e0e9cf6b61f35734f4dc2e2a8cf1ea876854b tuned diff -r 524e0e9cf6b6 -r 2a803a1556d5 QuotMain.thy --- a/QuotMain.thy Tue Oct 27 14:15:40 2009 +0100 +++ b/QuotMain.thy Tue Oct 27 14:46:38 2009 +0100 @@ -152,7 +152,7 @@ ML {* val quot_def_parser = (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- - ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) -- + ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- (OuterParse.binding -- Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) diff -r 524e0e9cf6b6 -r 2a803a1556d5 quotient.ML --- a/quotient.ML Tue Oct 27 14:15:40 2009 +0100 +++ b/quotient.ML Tue Oct 27 14:46:38 2009 +0100 @@ -103,7 +103,7 @@ -(* wrappers for define, note and theorem_i*) +(* wrappers for define, note and theorem_i *) fun define (name, mx, rhs) lthy = let val ((rhs, (_ , thm)), lthy') = @@ -163,7 +163,7 @@ (* tactic to prove the QUOT_TYPE theorem for the new type *) fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = let - val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def} + val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}] val rep_thm = #Rep typedef_info |> unfold_mem val rep_inv = #Rep_inverse typedef_info val abs_inv = #Abs_inverse typedef_info |> unfold_mem @@ -300,27 +300,26 @@ in theorem after_qed goals lthy end + +fun mk_quotient_type_cmd spec lthy = +let + fun parse_spec (((qty_str, mx), rty_str), rel_str) = + let + val qty_name = Binding.name qty_str + val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy + val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy + in + ((qty_name, mx), (rty, rel)) + end +in + mk_quotient_type (map parse_spec spec) lthy +end val quotspec_parser = OuterParse.and_list1 (OuterParse.short_ident -- OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- (OuterParse.$$$ "/" |-- OuterParse.term)) - -fun mk_quotient_type_cmd spec lthy = -let - fun parse_spec (((qty_str, mx), rty_str), rel_str) = - let - val qty_name = Binding.name qty_str - val rty = Syntax.parse_typ lthy rty_str - val rel = Syntax.parse_term lthy rel_str - |> Syntax.check_term lthy - in - ((qty_name, mx), (rty, rel)) - end -in - mk_quotient_type (map parse_spec spec) lthy -end val _ = OuterKeyword.keyword "/"