# HG changeset patch # User wenzelm # Date 1086086030 -7200 # Node ID 61bdf2ae4dc59a829b6f9da818eb645c0aff9571 # Parent 8d710bece29f50c505ebcc243236e7f75912578f removed obsolete sort 'logic'; diff -r 8d710bece29f -r 61bdf2ae4dc5 NEWS --- a/NEWS Tue Jun 01 11:25:26 2004 +0200 +++ b/NEWS Tue Jun 01 12:33:50 2004 +0200 @@ -32,6 +32,11 @@ instead of 'nonterminals'/'syntax'. Some very exotic syntax specifications may require further adaption (e.g. Cube/Base.thy). +* Pure: removed obsolete type class "logic", use the top sort {} + instead. Note that non-logical types should be declared as + 'nonterminals' rather than 'types'. INCOMPATIBILITY for new + object-logic specifications. + * Pure/Syntax: inner syntax includes (*(*nested*) comments*). * Pure/Syntax: pretty pinter now supports unbreakable blocks, diff -r 8d710bece29f -r 61bdf2ae4dc5 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/CTT/CTT.thy Tue Jun 01 12:33:50 2004 +0200 @@ -13,9 +13,6 @@ t o -arities - i,t,o :: logic - consts (*Types*) F,T :: "t" (*F is empty, T contains one element*) diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Cube/Base.thy --- a/src/Cube/Base.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Cube/Base.thy Tue Jun 01 12:33:50 2004 +0200 @@ -10,8 +10,6 @@ types term -arities - term :: logic types context typing diff -r 8d710bece29f -r 61bdf2ae4dc5 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/FOL/IFOL.thy Tue Jun 01 12:33:50 2004 +0200 @@ -13,7 +13,7 @@ global -classes "term" < logic +classes "term" defaultsort "term" typedecl o @@ -264,7 +264,7 @@ nonterminals letbinds letbind constdefs - Let :: "['a::logic, 'a => 'b] => ('b::logic)" + Let :: "['a::{}, 'a => 'b] => ('b::{})" "Let(s, f) == f(s)" syntax diff -r 8d710bece29f -r 61bdf2ae4dc5 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/FOLP/IFOLP.thy Tue Jun 01 12:33:50 2004 +0200 @@ -10,17 +10,13 @@ global -classes term < logic - +classes term default term types p o -arities - p,o :: logic - consts (*** Judgements ***) "@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5) diff -r 8d710bece29f -r 61bdf2ae4dc5 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/HOL/HOL.thy Tue Jun 01 12:33:50 2004 +0200 @@ -14,7 +14,7 @@ subsubsection {* Core syntax *} -classes type < logic +classes type defaultsort type global diff -r 8d710bece29f -r 61bdf2ae4dc5 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/HOL/Import/shuffler.ML Tue Jun 01 12:33:50 2004 +0200 @@ -132,8 +132,8 @@ val def_norm = let val cert = cterm_of (sign_of ProtoPure.thy) - val aT = TFree("'a",logicS) - val bT = TFree("'b",logicS) + val aT = TFree("'a",[]) + val bT = TFree("'b",[]) val v = Free("v",aT) val P = Free("P",aT-->bT) val Q = Free("Q",aT-->bT) @@ -159,8 +159,8 @@ val all_comm = let val cert = cterm_of (sign_of ProtoPure.thy) - val xT = TFree("'a",logicS) - val yT = TFree("'b",logicS) + val xT = TFree("'a",[]) + val yT = TFree("'b",[]) val P = Free("P",xT-->yT-->propT) val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0)))) val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1)))) @@ -404,7 +404,7 @@ end handle e => (writeln "eta_expand internal error";print_exn e) -fun mk_tfree s = TFree("'"^s,logicS) +fun mk_tfree s = TFree("'"^s,[]) val xT = mk_tfree "a" val yT = mk_tfree "b" val P = Var(("P",0),xT-->yT-->propT) @@ -495,8 +495,6 @@ end handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e) -fun is_logic_var sg v = - Type.of_sort (Sign.tsig_of sg) (type_of v,logicS) (* Closes a theorem with respect to free and schematic variables (does not touch type variables, though). *) @@ -505,10 +503,9 @@ let val sg = sign_of_thm th val c = prop_of th - val all_vars = add_term_frees (c,add_term_vars(c,[])) - val all_rel_vars = filter (is_logic_var sg) all_vars + val vars = add_term_frees (c,add_term_vars(c,[])) in - Drule.forall_intr_list (map (cterm_of sg) all_rel_vars) th + Drule.forall_intr_list (map (cterm_of sg) vars) th end handle e => (writeln "close_thm internal error"; print_exn e) @@ -572,10 +569,9 @@ fun set_prop thy t = let val sg = sign_of thy - val all_vars = add_term_frees (t,add_term_vars (t,[])) - val all_rel_vars = filter (is_logic_var sg) all_vars + val vars = add_term_frees (t,add_term_vars (t,[])) val closed_t = foldr (fn (v,body) => let val vT = type_of v - in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (all_rel_vars,t) + in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t) val rew_th = norm_term thy closed_t val rhs = snd (dest_equals (cprop_of rew_th)) @@ -596,7 +592,7 @@ val closed_th = equal_elim (symmetric rew_th) mod_th in message ("Shuffler.set_prop succeeded by " ^ name); - Some (name,forall_elim_list (map (cterm_of sg) all_rel_vars) closed_th) + Some (name,forall_elim_list (map (cterm_of sg) vars) closed_th) end | None => process thms end diff -r 8d710bece29f -r 61bdf2ae4dc5 src/HOL/Modelcheck/MuckeSyn.thy --- a/src/HOL/Modelcheck/MuckeSyn.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Tue Jun 01 12:33:50 2004 +0200 @@ -32,7 +32,7 @@ "ALL " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10) "EX " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10) - "_lambda" :: [idts, 'a::logic] => 'b::logic ("(3L _./ _)" 10) + "_lambda" :: [idts, 'a] => 'b ("(3L _./ _)" 10) "_applC" :: [('b => 'a), cargs] => aprop ("(1_/ '(_'))" [1000,1000] 999) "_cargs" :: ['a, cargs] => cargs ("_,/ _" [1000,1000] 1000) diff -r 8d710bece29f -r 61bdf2ae4dc5 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/HOL/Tools/record_package.ML Tue Jun 01 12:33:50 2004 +0200 @@ -615,7 +615,7 @@ val tsig = Sign.tsig_of sg fun mk_type_abbr subst name alphas = - let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas); + let val abbrT = Type (name, map (fn a => TVar ((a, 0), [])) alphas); in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end; fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T)) diff -r 8d710bece29f -r 61bdf2ae4dc5 src/HOL/ex/Higher_Order_Logic.thy --- a/src/HOL/ex/Higher_Order_Logic.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/HOL/ex/Higher_Order_Logic.thy Tue Jun 01 12:33:50 2004 +0200 @@ -20,7 +20,7 @@ subsection {* Pure Logic *} -classes type \ logic +classes type defaultsort type typedecl o diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Provers/splitter.ML Tue Jun 01 12:33:50 2004 +0200 @@ -76,8 +76,8 @@ val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; val lift = let val ct = read_cterm (#sign(rep_thm Data.iffD)) - ("[| !!x. (Q::('b::logic)=>('c::logic))(x) == R(x) |] ==> \ - \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT) + ("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \ + \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT) in prove_goalw_cterm [] ct (fn [prem] => [rewtac prem, rtac reflexive_thm 1]) end; diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/Isar/object_logic.ML Tue Jun 01 12:33:50 2004 +0200 @@ -115,7 +115,7 @@ fun fixed_judgment sg x = let (*be robust wrt. low-level errors*) val c = judgment_name sg; - val aT = TFree ("'a", logicS); + val aT = TFree ("'a", []); val T = if_none (Sign.const_type sg c) (aT --> propT) |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S)); diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Jun 01 12:33:50 2004 +0200 @@ -42,12 +42,11 @@ |> Theory.copy |> Theory.root_path |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)] - |> Theory.add_arities [("Type", [], "logic"), ("Null", [], "logic")] |> Theory.add_consts - [("typeof", "'b::logic => Type", NoSyn), - ("Type", "'a::logic itself => Type", NoSyn), + [("typeof", "'b::{} => Type", NoSyn), + ("Type", "'a::{} itself => Type", NoSyn), ("Null", "Null", NoSyn), - ("realizes", "'a::logic => 'b::logic => 'b", NoSyn)]; + ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)]; val nullT = Type ("Null", []); val nullt = Const ("Null", nullT); diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jun 01 12:33:50 2004 +0200 @@ -34,7 +34,7 @@ val paramT = Type ("param", []); val paramsT = Type ("params", []); val idtT = Type ("idt", []); -val aT = TFree ("'a", ["logic"]); +val aT = TFree ("'a", []); (** constants for theorems and axioms **) @@ -49,9 +49,8 @@ sg |> Sign.copy |> Sign.add_path "/" - |> Sign.add_defsort_i ["logic"] + |> Sign.add_defsort_i [] |> Sign.add_types [("proof", 0, NoSyn)] - |> Sign.add_arities [("proof", [], "logic")] |> Sign.add_consts_i [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/Proof/reconstruct.ML Tue Jun 01 12:33:50 2004 +0200 @@ -162,7 +162,7 @@ | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = let val (env', T) = (case opT of - None => mk_tvar (env, logicS) | Some T => (env, T)); + None => mk_tvar (env, []) | Some T => (env, T)); val (t, prf, cnstrts, env'', vTs') = mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, Some T, prf), @@ -216,7 +216,7 @@ end | (u, prf, cnstrts, env', vTs') => let - val (env1, T) = mk_tvar (env', ["logic"]); + val (env1, T) = mk_tvar (env', []); val (env2, v) = mk_var env1 Ts (T --> propT); val (env3, t) = mk_var env2 Ts T in diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/axclass.ML Tue Jun 01 12:33:50 2004 +0200 @@ -214,9 +214,6 @@ (* errors *) -fun err_not_logic c = - error ("Axiomatic class " ^ quote c ^ " not subclass of " ^ quote logicC); - fun err_bad_axsort ax c = error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c); @@ -243,19 +240,16 @@ (*prepare abstract axioms*) fun abs_axm ax = if null (term_tfrees ax) then - Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax) + Logic.mk_implies (Logic.mk_inclass (aT [], class), ax) else map_term_tfrees (K (aT [class])) ax; val abs_axms = map (abs_axm o #2) axms; - (*prepare introduction rule*) - val _ = if Sign.subsort class_sign ([class], logicS) then () else err_not_logic class; - fun axm_sort (name, ax) = (case term_tfrees ax of [] => [] | [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class | _ => err_bad_tfrees name); - val axS = Sign.certify_sort class_sign (logicC :: flat (map axm_sort axms)); + val axS = Sign.certify_sort class_sign (flat (map axm_sort axms)); val int_axm = Logic.close_form o map_term_tfrees (K (aT axS)); fun inclass c = Logic.mk_inclass (aT axS, c); diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/drule.ML Tue Jun 01 12:33:50 2004 +0200 @@ -548,16 +548,16 @@ fun store_standard_thm_open name thm = store_thm_open name (standard' thm); val reflexive_thm = - let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS))) + let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),[]))) in store_standard_thm_open "reflexive" (Thm.reflexive cx) end; val symmetric_thm = - let val xy = read_prop "x::'a::logic == y" + let val xy = read_prop "x == y" in store_standard_thm_open "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end; val transitive_thm = - let val xy = read_prop "x::'a::logic == y" - val yz = read_prop "y::'a::logic == z" + let val xy = read_prop "x == y" + val yz = read_prop "y == z" val xythm = Thm.assume xy and yzthm = Thm.assume yz in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; @@ -698,7 +698,7 @@ val norm_hhf_eq = let val cert = Thm.cterm_of proto_sign; - val aT = TFree ("'a", Term.logicS); + val aT = TFree ("'a", []); val all = Term.all aT; val x = Free ("x", aT); val phi = Free ("phi", propT); diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/proofterm.ML Tue Jun 01 12:33:50 2004 +0200 @@ -685,8 +685,8 @@ (***** axioms for equality *****) -val aT = TFree ("'a", ["logic"]); -val bT = TFree ("'b", ["logic"]); +val aT = TFree ("'a", []); +val bT = TFree ("'b", []); val x = Free ("x", aT); val y = Free ("y", aT); val z = Free ("z", aT); diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/pure_thy.ML Tue Jun 01 12:33:50 2004 +0200 @@ -500,17 +500,7 @@ fun type_of (raw_name, vs, mx) = if null (duplicates vs) then (raw_name, length vs, mx) else error ("Duplicate parameters in type declaration: " ^ quote raw_name); - - fun arity_of (raw_name, len, mx) = - (full (Syntax.type_name raw_name mx), replicate len logicS, logicS); - - val types = map type_of decls; - val arities = map arity_of types; - in - thy - |> Theory.add_types types - |> Theory.add_arities_i arities - end; + in thy |> Theory.add_types (map type_of decls) end; @@ -531,12 +521,6 @@ ("prop", 0, NoSyn), ("itself", 1, NoSyn), ("dummy", 0, NoSyn)] - |> Theory.add_classes_i [(logicC, [])] - |> Theory.add_defsort_i logicS - |> Theory.add_arities_i - [("fun", [logicS, logicS], logicS), - ("prop", [], logicS), - ("itself", [logicS], logicS)] |> Theory.add_nonterminals Syntax.pure_nonterms |> Theory.add_syntax Syntax.pure_syntax |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax @@ -544,17 +528,17 @@ [("==>", "[prop, prop] => prop", Delimfix "op ==>"), (Term.dummy_patternN, "aprop", Delimfix "'_")] |> Theory.add_consts - [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)), + [("==", "['a, 'a] => prop", InfixrName ("==", 2)), ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), ("all", "('a => prop) => prop", Binder ("!!", 0, 0)), ("Goal", "prop => prop", NoSyn), ("TYPE", "'a itself", NoSyn), (Term.dummy_patternN, "'a", Delimfix "'_")] |> Theory.add_finals_i false - [Const("==",[TFree("'a",[]),TFree("'a",[])]--->propT), - Const("==>",[propT,propT]--->propT), - Const("all",(TFree("'a",logicS)-->propT)-->propT), - Const("TYPE",a_itselfT)] + [Const("==", [TFree ("'a", []), TFree ("'a", [])] ---> propT), + Const("==>", [propT, propT] ---> propT), + Const("all", (TFree("'a", []) --> propT) --> propT), + Const("TYPE", a_itselfT)] |> Theory.add_modesyntax ("", false) (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax) |> Theory.add_trfuns Syntax.pure_trfuns diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/term.ML --- a/src/Pure/term.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/term.ML Tue Jun 01 12:33:50 2004 +0200 @@ -76,8 +76,6 @@ val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term val dummyT: typ - val logicC: class - val logicS: sort val itselfT: typ -> typ val a_itselfT: typ val propT: typ @@ -415,11 +413,8 @@ (** Connectives of higher order logic **) -val logicC: class = "logic"; -val logicS: sort = [logicC]; - fun itselfT ty = Type ("itself", [ty]); -val a_itselfT = itselfT (TFree ("'a", logicS)); +val a_itselfT = itselfT (TFree ("'a", [])); val propT : typ = Type("prop",[]); diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Pure/type_infer.ML Tue Jun 01 12:33:50 2004 +0200 @@ -103,7 +103,7 @@ (* pretyp(s)_of *) fun anyT S = TFree ("'_dummy_", S); -val logicT = anyT logicS; +val logicT = anyT []; (*indicate polymorphic Vars*) fun polymorphicT T = Type ("_polymorphic_", [T]); diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Sequents/ILL/ILL_predlog.thy --- a/src/Sequents/ILL/ILL_predlog.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Sequents/ILL/ILL_predlog.thy Tue Jun 01 12:33:50 2004 +0200 @@ -7,13 +7,8 @@ ILL_predlog = ILL + types - plf -arities - - plf :: logic - consts "&" :: "[plf,plf] => plf" (infixr 35) diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Sequents/LK0.thy Tue Jun 01 12:33:50 2004 +0200 @@ -13,11 +13,8 @@ global -classes - term < logic - -default - term +classes term +default term consts diff -r 8d710bece29f -r 61bdf2ae4dc5 src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/Sequents/Sequents.thy Tue Jun 01 12:33:50 2004 +0200 @@ -14,9 +14,6 @@ types o -arities - o :: logic - (* Sequences *) diff -r 8d710bece29f -r 61bdf2ae4dc5 src/ZF/Constructible/MetaExists.thy --- a/src/ZF/Constructible/MetaExists.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/ZF/Constructible/MetaExists.thy Tue Jun 01 12:33:50 2004 +0200 @@ -11,7 +11,7 @@ quantify over classes. Yields a proposition rather than a FOL formula.*} constdefs - ex :: "(('a::logic) => prop) => prop" (binder "?? " 0) + ex :: "(('a::{}) => prop) => prop" (binder "?? " 0) "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)" syntax (xsymbols) diff -r 8d710bece29f -r 61bdf2ae4dc5 src/ZF/QPair.thy --- a/src/ZF/QPair.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/ZF/QPair.thy Tue Jun 01 12:33:50 2004 +0200 @@ -31,7 +31,7 @@ qsnd :: "i => i" "qsnd(p) == THE b. EX a. p=" - qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*) + qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*for pattern-matching*) "qsplit(c,p) == c(qfst(p), qsnd(p))" qconverse :: "i => i" diff -r 8d710bece29f -r 61bdf2ae4dc5 src/ZF/ZF.thy --- a/src/ZF/ZF.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/ZF/ZF.thy Tue Jun 01 12:33:50 2004 +0200 @@ -61,7 +61,7 @@ Pair :: "[i, i] => i" fst :: "i => i" snd :: "i => i" - split :: "[[i, i] => 'a, i] => 'a::logic" --{*for pattern-matching*} + split :: "[[i, i] => 'a, i] => 'a::{}" --{*for pattern-matching*} text {*Sigma and Pi Operators *} consts