# HG changeset patch # User haftmann # Date 1232577757 -3600 # Node ID 9891e3646809346aa1f78074214c843a893f631c # Parent 2db3537c35359b6de460d4a3de1ed90766a986a0# Parent 83d282f12352733d7da8876427237acb911fad96 merged diff -r 2db3537c3535 -r 9891e3646809 NEWS --- a/NEWS Wed Jan 21 23:25:17 2009 +0100 +++ b/NEWS Wed Jan 21 23:42:37 2009 +0100 @@ -66,6 +66,12 @@ *** Pure *** +* Class declaration: sc. "base sort" must not be given in import list +any longer but is inferred from the specification. Particularly in HOL, +write + + class foo = ... instead of class foo = type + ... + * Type Binding.T gradually replaces formerly used type bstring for names to be bound. Name space interface for declarations has been simplified: diff -r 2db3537c3535 -r 9891e3646809 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/ATP_Linkup.thy Wed Jan 21 23:42:37 2009 +0100 @@ -7,7 +7,7 @@ header {* The Isabelle-ATP Linkup *} theory ATP_Linkup -imports Record Hilbert_Choice +imports Divides Record Hilbert_Choice uses "Tools/polyhash.ML" "Tools/res_clause.ML" diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Datatype.thy Wed Jan 21 23:42:37 2009 +0100 @@ -8,7 +8,7 @@ header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *} theory Datatype -imports Nat Relation +imports Nat Product_Type begin typedef (Node) @@ -509,15 +509,6 @@ lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard] -(*** Domain ***) - -lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)" -by auto - -lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)" -by auto - - text {* hides popular names *} hide (open) type node item hide (open) const Push Node Atom Leaf Numb Lim Split Case diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Finite_Set.thy Wed Jan 21 23:42:37 2009 +0100 @@ -6,7 +6,7 @@ header {* Finite sets *} theory Finite_Set -imports Datatype Divides Transitive_Closure +imports Nat Product_Type Power begin subsection {* Definition and basic properties *} @@ -380,46 +380,6 @@ by(blast intro: finite_subset[OF subset_Pow_Union]) -lemma finite_converse [iff]: "finite (r^-1) = finite r" - apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r") - apply simp - apply (rule iffI) - apply (erule finite_imageD [unfolded inj_on_def]) - apply (simp split add: split_split) - apply (erule finite_imageI) - apply (simp add: converse_def image_def, auto) - apply (rule bexI) - prefer 2 apply assumption - apply simp - done - - -text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi -Ehmety) *} - -lemma finite_Field: "finite r ==> finite (Field r)" - -- {* A finite relation has a finite field (@{text "= domain \ range"}. *} - apply (induct set: finite) - apply (auto simp add: Field_def Domain_insert Range_insert) - done - -lemma trancl_subset_Field2: "r^+ <= Field r \ Field r" - apply clarify - apply (erule trancl_induct) - apply (auto simp add: Field_def) - done - -lemma finite_trancl: "finite (r^+) = finite r" - apply auto - prefer 2 - apply (rule trancl_subset_Field2 [THEN finite_subset]) - apply (rule finite_SigmaI) - prefer 3 - apply (blast intro: r_into_trancl' finite_subset) - apply (auto simp add: finite_Field) - done - - subsection {* Class @{text finite} *} setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*} @@ -471,9 +431,6 @@ instance "+" :: (finite, finite) finite by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) -instance option :: (finite) finite - by default (simp add: insert_None_conv_UNIV [symmetric]) - subsection {* A fold functional for finite sets *} diff -r 2db3537c3535 -r 9891e3646809 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/HOL.thy Wed Jan 21 23:42:37 2009 +0100 @@ -208,34 +208,34 @@ subsubsection {* Generic classes and algebraic operations *} -class default = type + +class default = fixes default :: 'a -class zero = type + +class zero = fixes zero :: 'a ("0") -class one = type + +class one = fixes one :: 'a ("1") hide (open) const zero one -class plus = type + +class plus = fixes plus :: "'a \ 'a \ 'a" (infixl "+" 65) -class minus = type + +class minus = fixes minus :: "'a \ 'a \ 'a" (infixl "-" 65) -class uminus = type + +class uminus = fixes uminus :: "'a \ 'a" ("- _" [81] 80) -class times = type + +class times = fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) -class inverse = type + +class inverse = fixes inverse :: "'a \ 'a" and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) -class abs = type + +class abs = fixes abs :: "'a \ 'a" begin @@ -247,10 +247,10 @@ end -class sgn = type + +class sgn = fixes sgn :: "'a \ 'a" -class ord = type + +class ord = fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" begin @@ -1675,7 +1675,7 @@ text {* Equality *} -class eq = type + +class eq = fixes eq :: "'a \ 'a \ bool" assumes eq_equals: "eq x y \ x = y" begin diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Int.thy Wed Jan 21 23:42:37 2009 +0100 @@ -599,7 +599,7 @@ Bit1 :: "int \ int" where [code del]: "Bit1 k = 1 + k + k" -class number = type + -- {* for numeric types: nat, int, real, \dots *} +class number = -- {* for numeric types: nat, int, real, \dots *} fixes number_of :: "int \ 'a" use "Tools/numeral.ML" diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Library/Eval_Witness.thy --- a/src/HOL/Library/Eval_Witness.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Library/Eval_Witness.thy Wed Jan 21 23:42:37 2009 +0100 @@ -32,7 +32,7 @@ with the oracle. *} -class ml_equiv = type +class ml_equiv text {* Instances of @{text "ml_equiv"} should only be declared for those types, diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Library/Quotient.thy --- a/src/HOL/Library/Quotient.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Library/Quotient.thy Wed Jan 21 23:42:37 2009 +0100 @@ -21,7 +21,7 @@ "\ :: 'a => 'a => bool"}. *} -class eqv = type + +class eqv = fixes eqv :: "'a \ 'a \ bool" (infixl "\" 50) class equiv = eqv + diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Nat.thy Wed Jan 21 23:42:37 2009 +0100 @@ -1515,7 +1515,7 @@ subsection {* size of a datatype value *} -class size = type + +class size = fixes size :: "'a \ nat" -- {* see further theory @{text Wellfounded} *} end diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Nominal/Examples/W.thy --- a/src/HOL/Nominal/Examples/W.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Nominal/Examples/W.thy Wed Jan 21 23:42:37 2009 +0100 @@ -49,7 +49,7 @@ text {* free type variables *} -class ftv = type + +class ftv = fixes ftv :: "'a \ tvar list" instantiation * :: (ftv, ftv) ftv diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Parity.thy Wed Jan 21 23:42:37 2009 +0100 @@ -8,7 +8,7 @@ imports Plain Presburger begin -class even_odd = type + +class even_odd = fixes even :: "'a \ bool" abbreviation diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Plain.thy --- a/src/HOL/Plain.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Plain.thy Wed Jan 21 23:42:37 2009 +0100 @@ -1,7 +1,7 @@ header {* Plain HOL *} theory Plain -imports Datatype FunDef Record SAT Extraction +imports Datatype FunDef Record SAT Extraction Divides begin text {* @@ -9,6 +9,9 @@ include @{text Hilbert_Choice}. *} +instance option :: (finite) finite + by default (simp add: insert_None_conv_UNIV [symmetric]) + ML {* path_add "~~/src/HOL/Library" *} end diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Power.thy --- a/src/HOL/Power.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Power.thy Wed Jan 21 23:42:37 2009 +0100 @@ -11,7 +11,7 @@ imports Nat begin -class power = type + +class power = fixes power :: "'a \ nat \ 'a" (infixr "^" 80) subsection{*Powers for Arbitrary Monoids*} diff -r 2db3537c3535 -r 9891e3646809 src/HOL/RealVector.thy --- a/src/HOL/RealVector.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/RealVector.thy Wed Jan 21 23:42:37 2009 +0100 @@ -124,7 +124,7 @@ subsection {* Real vector spaces *} -class scaleR = type + +class scaleR = fixes scaleR :: "real \ 'a \ 'a" (infixr "*\<^sub>R" 75) begin @@ -418,7 +418,7 @@ subsection {* Real normed vector spaces *} -class norm = type + +class norm = fixes norm :: "'a \ real" instantiation real :: norm diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Relation.thy Wed Jan 21 23:42:37 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Relation.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) @@ -7,7 +6,7 @@ header {* Relations *} theory Relation -imports Product_Type +imports Datatype Finite_Set begin subsection {* Definitions *} @@ -379,6 +378,12 @@ lemma fst_eq_Domain: "fst ` R = Domain R"; by (auto intro!:image_eqI) +lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)" +by auto + +lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)" +by auto + subsection {* Range *} @@ -566,6 +571,31 @@ done +subsection {* Finiteness *} + +lemma finite_converse [iff]: "finite (r^-1) = finite r" + apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r") + apply simp + apply (rule iffI) + apply (erule finite_imageD [unfolded inj_on_def]) + apply (simp split add: split_split) + apply (erule finite_imageI) + apply (simp add: converse_def image_def, auto) + apply (rule bexI) + prefer 2 apply assumption + apply simp + done + +text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi +Ehmety) *} + +lemma finite_Field: "finite r ==> finite (Field r)" + -- {* A finite relation has a finite field (@{text "= domain \ range"}. *} + apply (induct set: finite) + apply (auto simp add: Field_def Domain_insert Range_insert) + done + + subsection {* Version of @{text lfp_induct} for binary relations *} lemmas lfp_induct2 = diff -r 2db3537c3535 -r 9891e3646809 src/HOL/SizeChange/Kleene_Algebras.thy --- a/src/HOL/SizeChange/Kleene_Algebras.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/SizeChange/Kleene_Algebras.thy Wed Jan 21 23:42:37 2009 +0100 @@ -11,7 +11,7 @@ text {* A type class of kleene algebras *} -class star = type + +class star = fixes star :: "'a \ 'a" class idem_add = ab_semigroup_add + diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Transitive_Closure.thy Wed Jan 21 23:42:37 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Transitive_Closure.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) @@ -568,6 +567,22 @@ apply auto done +lemma trancl_subset_Field2: "r^+ <= Field r \ Field r" + apply clarify + apply (erule trancl_induct) + apply (auto simp add: Field_def) + done + +lemma finite_trancl: "finite (r^+) = finite r" + apply auto + prefer 2 + apply (rule trancl_subset_Field2 [THEN finite_subset]) + apply (rule finite_SigmaI) + prefer 3 + apply (blast intro: r_into_trancl' finite_subset) + apply (auto simp add: finite_Field) + done + text {* More about converse @{text rtrancl} and @{text trancl}, should be merged with main body. *} diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Typedef.thy --- a/src/HOL/Typedef.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Typedef.thy Wed Jan 21 23:42:37 2009 +0100 @@ -123,7 +123,7 @@ text {* This class is just a workaround for classes without parameters; it shall disappear as soon as possible. *} -class itself = type + +class itself = fixes itself :: "'a itself" setup {* diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Wellfounded.thy Wed Jan 21 23:42:37 2009 +0100 @@ -7,7 +7,7 @@ header {*Well-founded Recursion*} theory Wellfounded -imports Finite_Set Nat +imports Finite_Set Transitive_Closure Nat uses ("Tools/function_package/size.ML") begin diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Word/BitSyntax.thy --- a/src/HOL/Word/BitSyntax.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Word/BitSyntax.thy Wed Jan 21 23:42:37 2009 +0100 @@ -12,7 +12,7 @@ imports BinGeneral begin -class bit = type + +class bit = fixes bitNOT :: "'a \ 'a" ("NOT _" [70] 71) and bitAND :: "'a \ 'a \ 'a" (infixr "AND" 64) and bitOR :: "'a \ 'a \ 'a" (infixr "OR" 59) diff -r 2db3537c3535 -r 9891e3646809 src/HOL/Word/Size.thy --- a/src/HOL/Word/Size.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOL/Word/Size.thy Wed Jan 21 23:42:37 2009 +0100 @@ -18,7 +18,7 @@ some duplication with the definitions in @{text "Numeral_Type"}. *} -class len0 = type + +class len0 = fixes len_of :: "'a itself \ nat" text {* diff -r 2db3537c3535 -r 9891e3646809 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Wed Jan 21 23:25:17 2009 +0100 +++ b/src/HOLCF/Porder.thy Wed Jan 21 23:42:37 2009 +0100 @@ -10,7 +10,7 @@ subsection {* Type class for partial orders *} -class sq_ord = type + +class sq_ord = fixes sq_le :: "'a \ 'a \ bool" notation diff -r 2db3537c3535 -r 9891e3646809 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Jan 21 23:25:17 2009 +0100 +++ b/src/Pure/Isar/class.ML Wed Jan 21 23:42:37 2009 +0100 @@ -92,8 +92,8 @@ fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt => let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end)); -fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) => - if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort) +val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) => + if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort) else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi) (*FIXME does not occur*) | T as TFree (v, sort) => @@ -119,11 +119,12 @@ let (* prepare import *) val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); - val (sups, others_basesort) = map (prep_class thy) raw_supclasses - |> Sign.minimize_sort thy - |> List.partition (is_class thy); - - val supparams = (map o apsnd) (snd o snd) (these_params thy sups); + val sups = map (prep_class thy) raw_supclasses + |> Sign.minimize_sort thy; + val _ = case filter_out (is_class thy) sups + of [] => () + | no_classes => error ("These are not classes: " ^ commas (map quote no_classes)); + val supparams = (map o apsnd) (snd o snd) (these_params thy sups); val supparam_names = map fst supparams; val _ = if has_duplicates (op =) supparam_names then error ("Duplicate parameter(s) in superclasses: " @@ -131,7 +132,7 @@ else (); val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); - val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort; + val given_basesort = fold inter_sort (map (base_sort thy) sups) []; (* infer types and base sort *) val base_constraints = (map o apsnd) @@ -139,10 +140,9 @@ (these_operations thy sups); val ((_, _, inferred_elems), _) = ProofContext.init thy |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints - |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort)) + |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param |> add_typ_check ~2 "singleton_fixate" singleton_fixate |> prep_decl supexpr raw_elems; - (*FIXME propagation of given base sort into class spec broken*) (*FIXME check for *all* side conditions here, extra check function for elements, less side-condition checks in check phase*) val base_sort = if null inferred_elems then given_basesort else @@ -170,45 +170,6 @@ val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration; val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration; -(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems = - let - (*FIXME 2009 simplify*) - val supclasses = map (prep_class thy) raw_supclasses; - val supsort = Sign.minimize_sort thy supclasses; - val (sups, bases) = List.partition (is_class thy) supsort; - val base_sort = if null sups then supsort else - Library.foldr (Sorts.inter_sort (Sign.classes_of thy)) - (map (base_sort thy) sups, bases); - val supparams = (map o apsnd) (snd o snd) (these_params thy sups); - val supparam_names = map fst supparams; - val _ = if has_duplicates (op =) supparam_names - then error ("Duplicate parameter(s) in superclasses: " - ^ (commas o map quote o duplicates (op =)) supparam_names) - else (); - - val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional []))) - sups, []); - val constrain = Element.Constrains ((map o apsnd o map_atyps) - (K (TFree (Name.aT, base_sort))) supparams); - (*FIXME 2009 perhaps better: control type variable by explicit - parameter instantiation of import expression*) - val begin_ctxt = begin sups base_sort - #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps) - (K (TFree (Name.aT, base_sort))) supparams) (*FIXME - should constraints be issued in begin?*) - val ((_, _, syntax_elems), _) = ProofContext.init thy - |> begin_ctxt - |> process_decl supexpr raw_elems; - fun fork_syn (Element.Fixes xs) = - fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs - #>> Element.Fixes - | fork_syn x = pair x; - val (elems, global_syntax) = fold_map fork_syn syntax_elems []; - in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end; - -val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration; -val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*) - fun add_consts bname class base_sort sups supparams global_syntax thy = let (*FIXME 2009 simplify*) diff -r 2db3537c3535 -r 9891e3646809 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Wed Jan 21 23:25:17 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Wed Jan 21 23:42:37 2009 +0100 @@ -55,8 +55,6 @@ -> (Attrib.binding * string list) list -> theory -> class * theory val classrel_cmd: xstring * xstring -> theory -> Proof.state - - (*old instance layer*) val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state end; @@ -275,7 +273,7 @@ val intros = (snd o rules thy) sup :: map_filter I [Option.map (Drule.standard' o Element.conclude_witness) some_wit, (fst o rules thy) sub]; - val tac = ALLGOALS (EVERY' (map Tactic.rtac intros)); + val tac = EVERY (map (TRYALL o Tactic.rtac) intros); val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) (K tac); val diff_sort = Sign.complete_sort thy [sup] @@ -285,9 +283,9 @@ |> AxClass.add_classrel classrel |> ClassData.map (Graph.add_edge (sub, sup)) |> activate_defs sub (these_defs thy diff_sort) - |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup, - dep_morph $> Element.satisfy_morphism [wit] $> export)) - (the_list some_dep_morph) (the_list some_wit) + |> fold (fn dep_morph => Locale.add_dependency sub (sup, + dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export)) + (the_list some_dep_morph) |> (fn thy => fold_rev Locale.activate_global_facts (Locale.get_registrations thy) thy) end; diff -r 2db3537c3535 -r 9891e3646809 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Jan 21 23:25:17 2009 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Jan 21 23:42:37 2009 +0100 @@ -428,7 +428,7 @@ val _ = OuterSyntax.command "class" "define type class" K.thy_decl - (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin + (P.name -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin >> (fn ((name, (supclasses, elems)), begin) => (begin ? Toplevel.print) o Toplevel.begin_local_theory begin (Class.class_cmd name supclasses elems #> snd)));