1.1 --- a/NEWS Tue Jun 01 11:25:26 2004 +0200
1.2 +++ b/NEWS Tue Jun 01 12:33:50 2004 +0200
1.3 @@ -32,6 +32,11 @@
1.4 instead of 'nonterminals'/'syntax'. Some very exotic syntax
1.5 specifications may require further adaption (e.g. Cube/Base.thy).
1.6
1.7 +* Pure: removed obsolete type class "logic", use the top sort {}
1.8 + instead. Note that non-logical types should be declared as
1.9 + 'nonterminals' rather than 'types'. INCOMPATIBILITY for new
1.10 + object-logic specifications.
1.11 +
1.12 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
1.13
1.14 * Pure/Syntax: pretty pinter now supports unbreakable blocks,
2.1 --- a/src/CTT/CTT.thy Tue Jun 01 11:25:26 2004 +0200
2.2 +++ b/src/CTT/CTT.thy Tue Jun 01 12:33:50 2004 +0200
2.3 @@ -13,9 +13,6 @@
2.4 t
2.5 o
2.6
2.7 -arities
2.8 - i,t,o :: logic
2.9 -
2.10 consts
2.11 (*Types*)
2.12 F,T :: "t" (*F is empty, T contains one element*)
3.1 --- a/src/Cube/Base.thy Tue Jun 01 11:25:26 2004 +0200
3.2 +++ b/src/Cube/Base.thy Tue Jun 01 12:33:50 2004 +0200
3.3 @@ -10,8 +10,6 @@
3.4
3.5 types
3.6 term
3.7 -arities
3.8 - term :: logic
3.9
3.10 types
3.11 context typing
4.1 --- a/src/FOL/IFOL.thy Tue Jun 01 11:25:26 2004 +0200
4.2 +++ b/src/FOL/IFOL.thy Tue Jun 01 12:33:50 2004 +0200
4.3 @@ -13,7 +13,7 @@
4.4
4.5 global
4.6
4.7 -classes "term" < logic
4.8 +classes "term"
4.9 defaultsort "term"
4.10
4.11 typedecl o
4.12 @@ -264,7 +264,7 @@
4.13 nonterminals letbinds letbind
4.14
4.15 constdefs
4.16 - Let :: "['a::logic, 'a => 'b] => ('b::logic)"
4.17 + Let :: "['a::{}, 'a => 'b] => ('b::{})"
4.18 "Let(s, f) == f(s)"
4.19
4.20 syntax
5.1 --- a/src/FOLP/IFOLP.thy Tue Jun 01 11:25:26 2004 +0200
5.2 +++ b/src/FOLP/IFOLP.thy Tue Jun 01 12:33:50 2004 +0200
5.3 @@ -10,17 +10,13 @@
5.4
5.5 global
5.6
5.7 -classes term < logic
5.8 -
5.9 +classes term
5.10 default term
5.11
5.12 types
5.13 p
5.14 o
5.15
5.16 -arities
5.17 - p,o :: logic
5.18 -
5.19 consts
5.20 (*** Judgements ***)
5.21 "@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5)
6.1 --- a/src/HOL/HOL.thy Tue Jun 01 11:25:26 2004 +0200
6.2 +++ b/src/HOL/HOL.thy Tue Jun 01 12:33:50 2004 +0200
6.3 @@ -14,7 +14,7 @@
6.4
6.5 subsubsection {* Core syntax *}
6.6
6.7 -classes type < logic
6.8 +classes type
6.9 defaultsort type
6.10
6.11 global
7.1 --- a/src/HOL/Import/shuffler.ML Tue Jun 01 11:25:26 2004 +0200
7.2 +++ b/src/HOL/Import/shuffler.ML Tue Jun 01 12:33:50 2004 +0200
7.3 @@ -132,8 +132,8 @@
7.4 val def_norm =
7.5 let
7.6 val cert = cterm_of (sign_of ProtoPure.thy)
7.7 - val aT = TFree("'a",logicS)
7.8 - val bT = TFree("'b",logicS)
7.9 + val aT = TFree("'a",[])
7.10 + val bT = TFree("'b",[])
7.11 val v = Free("v",aT)
7.12 val P = Free("P",aT-->bT)
7.13 val Q = Free("Q",aT-->bT)
7.14 @@ -159,8 +159,8 @@
7.15 val all_comm =
7.16 let
7.17 val cert = cterm_of (sign_of ProtoPure.thy)
7.18 - val xT = TFree("'a",logicS)
7.19 - val yT = TFree("'b",logicS)
7.20 + val xT = TFree("'a",[])
7.21 + val yT = TFree("'b",[])
7.22 val P = Free("P",xT-->yT-->propT)
7.23 val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
7.24 val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
7.25 @@ -404,7 +404,7 @@
7.26 end
7.27 handle e => (writeln "eta_expand internal error";print_exn e)
7.28
7.29 -fun mk_tfree s = TFree("'"^s,logicS)
7.30 +fun mk_tfree s = TFree("'"^s,[])
7.31 val xT = mk_tfree "a"
7.32 val yT = mk_tfree "b"
7.33 val P = Var(("P",0),xT-->yT-->propT)
7.34 @@ -495,8 +495,6 @@
7.35 end
7.36 handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
7.37
7.38 -fun is_logic_var sg v =
7.39 - Type.of_sort (Sign.tsig_of sg) (type_of v,logicS)
7.40
7.41 (* Closes a theorem with respect to free and schematic variables (does
7.42 not touch type variables, though). *)
7.43 @@ -505,10 +503,9 @@
7.44 let
7.45 val sg = sign_of_thm th
7.46 val c = prop_of th
7.47 - val all_vars = add_term_frees (c,add_term_vars(c,[]))
7.48 - val all_rel_vars = filter (is_logic_var sg) all_vars
7.49 + val vars = add_term_frees (c,add_term_vars(c,[]))
7.50 in
7.51 - Drule.forall_intr_list (map (cterm_of sg) all_rel_vars) th
7.52 + Drule.forall_intr_list (map (cterm_of sg) vars) th
7.53 end
7.54 handle e => (writeln "close_thm internal error"; print_exn e)
7.55
7.56 @@ -572,10 +569,9 @@
7.57 fun set_prop thy t =
7.58 let
7.59 val sg = sign_of thy
7.60 - val all_vars = add_term_frees (t,add_term_vars (t,[]))
7.61 - val all_rel_vars = filter (is_logic_var sg) all_vars
7.62 + val vars = add_term_frees (t,add_term_vars (t,[]))
7.63 val closed_t = foldr (fn (v,body) => let val vT = type_of v
7.64 - in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (all_rel_vars,t)
7.65 + in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t)
7.66 val rew_th = norm_term thy closed_t
7.67 val rhs = snd (dest_equals (cprop_of rew_th))
7.68
7.69 @@ -596,7 +592,7 @@
7.70 val closed_th = equal_elim (symmetric rew_th) mod_th
7.71 in
7.72 message ("Shuffler.set_prop succeeded by " ^ name);
7.73 - Some (name,forall_elim_list (map (cterm_of sg) all_rel_vars) closed_th)
7.74 + Some (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
7.75 end
7.76 | None => process thms
7.77 end
8.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy Tue Jun 01 11:25:26 2004 +0200
8.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Tue Jun 01 12:33:50 2004 +0200
8.3 @@ -32,7 +32,7 @@
8.4 "ALL " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10)
8.5 "EX " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10)
8.6
8.7 - "_lambda" :: [idts, 'a::logic] => 'b::logic ("(3L _./ _)" 10)
8.8 + "_lambda" :: [idts, 'a] => 'b ("(3L _./ _)" 10)
8.9 "_applC" :: [('b => 'a), cargs] => aprop ("(1_/ '(_'))" [1000,1000] 999)
8.10 "_cargs" :: ['a, cargs] => cargs ("_,/ _" [1000,1000] 1000)
8.11
9.1 --- a/src/HOL/Tools/record_package.ML Tue Jun 01 11:25:26 2004 +0200
9.2 +++ b/src/HOL/Tools/record_package.ML Tue Jun 01 12:33:50 2004 +0200
9.3 @@ -615,7 +615,7 @@
9.4 val tsig = Sign.tsig_of sg
9.5
9.6 fun mk_type_abbr subst name alphas =
9.7 - let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
9.8 + let val abbrT = Type (name, map (fn a => TVar ((a, 0), [])) alphas);
9.9 in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
9.10
9.11 fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
10.1 --- a/src/HOL/ex/Higher_Order_Logic.thy Tue Jun 01 11:25:26 2004 +0200
10.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy Tue Jun 01 12:33:50 2004 +0200
10.3 @@ -20,7 +20,7 @@
10.4
10.5 subsection {* Pure Logic *}
10.6
10.7 -classes type \<subseteq> logic
10.8 +classes type
10.9 defaultsort type
10.10
10.11 typedecl o
11.1 --- a/src/Provers/splitter.ML Tue Jun 01 11:25:26 2004 +0200
11.2 +++ b/src/Provers/splitter.ML Tue Jun 01 12:33:50 2004 +0200
11.3 @@ -76,8 +76,8 @@
11.4 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
11.5 val lift =
11.6 let val ct = read_cterm (#sign(rep_thm Data.iffD))
11.7 - ("[| !!x. (Q::('b::logic)=>('c::logic))(x) == R(x) |] ==> \
11.8 - \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
11.9 + ("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \
11.10 + \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
11.11 in prove_goalw_cterm [] ct
11.12 (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
11.13 end;
12.1 --- a/src/Pure/Isar/object_logic.ML Tue Jun 01 11:25:26 2004 +0200
12.2 +++ b/src/Pure/Isar/object_logic.ML Tue Jun 01 12:33:50 2004 +0200
12.3 @@ -115,7 +115,7 @@
12.4 fun fixed_judgment sg x =
12.5 let (*be robust wrt. low-level errors*)
12.6 val c = judgment_name sg;
12.7 - val aT = TFree ("'a", logicS);
12.8 + val aT = TFree ("'a", []);
12.9 val T =
12.10 if_none (Sign.const_type sg c) (aT --> propT)
12.11 |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
13.1 --- a/src/Pure/Proof/extraction.ML Tue Jun 01 11:25:26 2004 +0200
13.2 +++ b/src/Pure/Proof/extraction.ML Tue Jun 01 12:33:50 2004 +0200
13.3 @@ -42,12 +42,11 @@
13.4 |> Theory.copy
13.5 |> Theory.root_path
13.6 |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
13.7 - |> Theory.add_arities [("Type", [], "logic"), ("Null", [], "logic")]
13.8 |> Theory.add_consts
13.9 - [("typeof", "'b::logic => Type", NoSyn),
13.10 - ("Type", "'a::logic itself => Type", NoSyn),
13.11 + [("typeof", "'b::{} => Type", NoSyn),
13.12 + ("Type", "'a::{} itself => Type", NoSyn),
13.13 ("Null", "Null", NoSyn),
13.14 - ("realizes", "'a::logic => 'b::logic => 'b", NoSyn)];
13.15 + ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
13.16
13.17 val nullT = Type ("Null", []);
13.18 val nullt = Const ("Null", nullT);
14.1 --- a/src/Pure/Proof/proof_syntax.ML Tue Jun 01 11:25:26 2004 +0200
14.2 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jun 01 12:33:50 2004 +0200
14.3 @@ -34,7 +34,7 @@
14.4 val paramT = Type ("param", []);
14.5 val paramsT = Type ("params", []);
14.6 val idtT = Type ("idt", []);
14.7 -val aT = TFree ("'a", ["logic"]);
14.8 +val aT = TFree ("'a", []);
14.9
14.10 (** constants for theorems and axioms **)
14.11
14.12 @@ -49,9 +49,8 @@
14.13 sg
14.14 |> Sign.copy
14.15 |> Sign.add_path "/"
14.16 - |> Sign.add_defsort_i ["logic"]
14.17 + |> Sign.add_defsort_i []
14.18 |> Sign.add_types [("proof", 0, NoSyn)]
14.19 - |> Sign.add_arities [("proof", [], "logic")]
14.20 |> Sign.add_consts_i
14.21 [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
14.22 ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
15.1 --- a/src/Pure/Proof/reconstruct.ML Tue Jun 01 11:25:26 2004 +0200
15.2 +++ b/src/Pure/Proof/reconstruct.ML Tue Jun 01 12:33:50 2004 +0200
15.3 @@ -162,7 +162,7 @@
15.4 | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
15.5 let
15.6 val (env', T) = (case opT of
15.7 - None => mk_tvar (env, logicS) | Some T => (env, T));
15.8 + None => mk_tvar (env, []) | Some T => (env, T));
15.9 val (t, prf, cnstrts, env'', vTs') =
15.10 mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
15.11 in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, Some T, prf),
15.12 @@ -216,7 +216,7 @@
15.13 end
15.14 | (u, prf, cnstrts, env', vTs') =>
15.15 let
15.16 - val (env1, T) = mk_tvar (env', ["logic"]);
15.17 + val (env1, T) = mk_tvar (env', []);
15.18 val (env2, v) = mk_var env1 Ts (T --> propT);
15.19 val (env3, t) = mk_var env2 Ts T
15.20 in
16.1 --- a/src/Pure/axclass.ML Tue Jun 01 11:25:26 2004 +0200
16.2 +++ b/src/Pure/axclass.ML Tue Jun 01 12:33:50 2004 +0200
16.3 @@ -214,9 +214,6 @@
16.4
16.5 (* errors *)
16.6
16.7 -fun err_not_logic c =
16.8 - error ("Axiomatic class " ^ quote c ^ " not subclass of " ^ quote logicC);
16.9 -
16.10 fun err_bad_axsort ax c =
16.11 error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c);
16.12
16.13 @@ -243,19 +240,16 @@
16.14 (*prepare abstract axioms*)
16.15 fun abs_axm ax =
16.16 if null (term_tfrees ax) then
16.17 - Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax)
16.18 + Logic.mk_implies (Logic.mk_inclass (aT [], class), ax)
16.19 else map_term_tfrees (K (aT [class])) ax;
16.20 val abs_axms = map (abs_axm o #2) axms;
16.21
16.22 - (*prepare introduction rule*)
16.23 - val _ = if Sign.subsort class_sign ([class], logicS) then () else err_not_logic class;
16.24 -
16.25 fun axm_sort (name, ax) =
16.26 (case term_tfrees ax of
16.27 [] => []
16.28 | [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class
16.29 | _ => err_bad_tfrees name);
16.30 - val axS = Sign.certify_sort class_sign (logicC :: flat (map axm_sort axms));
16.31 + val axS = Sign.certify_sort class_sign (flat (map axm_sort axms));
16.32
16.33 val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
16.34 fun inclass c = Logic.mk_inclass (aT axS, c);
17.1 --- a/src/Pure/drule.ML Tue Jun 01 11:25:26 2004 +0200
17.2 +++ b/src/Pure/drule.ML Tue Jun 01 12:33:50 2004 +0200
17.3 @@ -548,16 +548,16 @@
17.4 fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
17.5
17.6 val reflexive_thm =
17.7 - let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
17.8 + let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),[])))
17.9 in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
17.10
17.11 val symmetric_thm =
17.12 - let val xy = read_prop "x::'a::logic == y"
17.13 + let val xy = read_prop "x == y"
17.14 in store_standard_thm_open "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
17.15
17.16 val transitive_thm =
17.17 - let val xy = read_prop "x::'a::logic == y"
17.18 - val yz = read_prop "y::'a::logic == z"
17.19 + let val xy = read_prop "x == y"
17.20 + val yz = read_prop "y == z"
17.21 val xythm = Thm.assume xy and yzthm = Thm.assume yz
17.22 in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
17.23
17.24 @@ -698,7 +698,7 @@
17.25 val norm_hhf_eq =
17.26 let
17.27 val cert = Thm.cterm_of proto_sign;
17.28 - val aT = TFree ("'a", Term.logicS);
17.29 + val aT = TFree ("'a", []);
17.30 val all = Term.all aT;
17.31 val x = Free ("x", aT);
17.32 val phi = Free ("phi", propT);
18.1 --- a/src/Pure/proofterm.ML Tue Jun 01 11:25:26 2004 +0200
18.2 +++ b/src/Pure/proofterm.ML Tue Jun 01 12:33:50 2004 +0200
18.3 @@ -685,8 +685,8 @@
18.4
18.5 (***** axioms for equality *****)
18.6
18.7 -val aT = TFree ("'a", ["logic"]);
18.8 -val bT = TFree ("'b", ["logic"]);
18.9 +val aT = TFree ("'a", []);
18.10 +val bT = TFree ("'b", []);
18.11 val x = Free ("x", aT);
18.12 val y = Free ("y", aT);
18.13 val z = Free ("z", aT);
19.1 --- a/src/Pure/pure_thy.ML Tue Jun 01 11:25:26 2004 +0200
19.2 +++ b/src/Pure/pure_thy.ML Tue Jun 01 12:33:50 2004 +0200
19.3 @@ -500,17 +500,7 @@
19.4 fun type_of (raw_name, vs, mx) =
19.5 if null (duplicates vs) then (raw_name, length vs, mx)
19.6 else error ("Duplicate parameters in type declaration: " ^ quote raw_name);
19.7 -
19.8 - fun arity_of (raw_name, len, mx) =
19.9 - (full (Syntax.type_name raw_name mx), replicate len logicS, logicS);
19.10 -
19.11 - val types = map type_of decls;
19.12 - val arities = map arity_of types;
19.13 - in
19.14 - thy
19.15 - |> Theory.add_types types
19.16 - |> Theory.add_arities_i arities
19.17 - end;
19.18 + in thy |> Theory.add_types (map type_of decls) end;
19.19
19.20
19.21
19.22 @@ -531,12 +521,6 @@
19.23 ("prop", 0, NoSyn),
19.24 ("itself", 1, NoSyn),
19.25 ("dummy", 0, NoSyn)]
19.26 - |> Theory.add_classes_i [(logicC, [])]
19.27 - |> Theory.add_defsort_i logicS
19.28 - |> Theory.add_arities_i
19.29 - [("fun", [logicS, logicS], logicS),
19.30 - ("prop", [], logicS),
19.31 - ("itself", [logicS], logicS)]
19.32 |> Theory.add_nonterminals Syntax.pure_nonterms
19.33 |> Theory.add_syntax Syntax.pure_syntax
19.34 |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
19.35 @@ -544,17 +528,17 @@
19.36 [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
19.37 (Term.dummy_patternN, "aprop", Delimfix "'_")]
19.38 |> Theory.add_consts
19.39 - [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
19.40 + [("==", "['a, 'a] => prop", InfixrName ("==", 2)),
19.41 ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
19.42 ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
19.43 ("Goal", "prop => prop", NoSyn),
19.44 ("TYPE", "'a itself", NoSyn),
19.45 (Term.dummy_patternN, "'a", Delimfix "'_")]
19.46 |> Theory.add_finals_i false
19.47 - [Const("==",[TFree("'a",[]),TFree("'a",[])]--->propT),
19.48 - Const("==>",[propT,propT]--->propT),
19.49 - Const("all",(TFree("'a",logicS)-->propT)-->propT),
19.50 - Const("TYPE",a_itselfT)]
19.51 + [Const("==", [TFree ("'a", []), TFree ("'a", [])] ---> propT),
19.52 + Const("==>", [propT, propT] ---> propT),
19.53 + Const("all", (TFree("'a", []) --> propT) --> propT),
19.54 + Const("TYPE", a_itselfT)]
19.55 |> Theory.add_modesyntax ("", false)
19.56 (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
19.57 |> Theory.add_trfuns Syntax.pure_trfuns
20.1 --- a/src/Pure/term.ML Tue Jun 01 11:25:26 2004 +0200
20.2 +++ b/src/Pure/term.ML Tue Jun 01 12:33:50 2004 +0200
20.3 @@ -76,8 +76,6 @@
20.4 val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
20.5 val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
20.6 val dummyT: typ
20.7 - val logicC: class
20.8 - val logicS: sort
20.9 val itselfT: typ -> typ
20.10 val a_itselfT: typ
20.11 val propT: typ
20.12 @@ -415,11 +413,8 @@
20.13
20.14 (** Connectives of higher order logic **)
20.15
20.16 -val logicC: class = "logic";
20.17 -val logicS: sort = [logicC];
20.18 -
20.19 fun itselfT ty = Type ("itself", [ty]);
20.20 -val a_itselfT = itselfT (TFree ("'a", logicS));
20.21 +val a_itselfT = itselfT (TFree ("'a", []));
20.22
20.23 val propT : typ = Type("prop",[]);
20.24
21.1 --- a/src/Pure/type_infer.ML Tue Jun 01 11:25:26 2004 +0200
21.2 +++ b/src/Pure/type_infer.ML Tue Jun 01 12:33:50 2004 +0200
21.3 @@ -103,7 +103,7 @@
21.4 (* pretyp(s)_of *)
21.5
21.6 fun anyT S = TFree ("'_dummy_", S);
21.7 -val logicT = anyT logicS;
21.8 +val logicT = anyT [];
21.9
21.10 (*indicate polymorphic Vars*)
21.11 fun polymorphicT T = Type ("_polymorphic_", [T]);
22.1 --- a/src/Sequents/ILL/ILL_predlog.thy Tue Jun 01 11:25:26 2004 +0200
22.2 +++ b/src/Sequents/ILL/ILL_predlog.thy Tue Jun 01 12:33:50 2004 +0200
22.3 @@ -7,13 +7,8 @@
22.4 ILL_predlog = ILL +
22.5
22.6 types
22.7 -
22.8 plf
22.9
22.10 -arities
22.11 -
22.12 - plf :: logic
22.13 -
22.14 consts
22.15
22.16 "&" :: "[plf,plf] => plf" (infixr 35)
23.1 --- a/src/Sequents/LK0.thy Tue Jun 01 11:25:26 2004 +0200
23.2 +++ b/src/Sequents/LK0.thy Tue Jun 01 12:33:50 2004 +0200
23.3 @@ -13,11 +13,8 @@
23.4
23.5 global
23.6
23.7 -classes
23.8 - term < logic
23.9 -
23.10 -default
23.11 - term
23.12 +classes term
23.13 +default term
23.14
23.15 consts
23.16
24.1 --- a/src/Sequents/Sequents.thy Tue Jun 01 11:25:26 2004 +0200
24.2 +++ b/src/Sequents/Sequents.thy Tue Jun 01 12:33:50 2004 +0200
24.3 @@ -14,9 +14,6 @@
24.4 types
24.5 o
24.6
24.7 -arities
24.8 - o :: logic
24.9 -
24.10
24.11 (* Sequences *)
24.12
25.1 --- a/src/ZF/Constructible/MetaExists.thy Tue Jun 01 11:25:26 2004 +0200
25.2 +++ b/src/ZF/Constructible/MetaExists.thy Tue Jun 01 12:33:50 2004 +0200
25.3 @@ -11,7 +11,7 @@
25.4 quantify over classes. Yields a proposition rather than a FOL formula.*}
25.5
25.6 constdefs
25.7 - ex :: "(('a::logic) => prop) => prop" (binder "?? " 0)
25.8 + ex :: "(('a::{}) => prop) => prop" (binder "?? " 0)
25.9 "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
25.10
25.11 syntax (xsymbols)
26.1 --- a/src/ZF/QPair.thy Tue Jun 01 11:25:26 2004 +0200
26.2 +++ b/src/ZF/QPair.thy Tue Jun 01 12:33:50 2004 +0200
26.3 @@ -31,7 +31,7 @@
26.4 qsnd :: "i => i"
26.5 "qsnd(p) == THE b. EX a. p=<a;b>"
26.6
26.7 - qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*)
26.8 + qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*for pattern-matching*)
26.9 "qsplit(c,p) == c(qfst(p), qsnd(p))"
26.10
26.11 qconverse :: "i => i"
27.1 --- a/src/ZF/ZF.thy Tue Jun 01 11:25:26 2004 +0200
27.2 +++ b/src/ZF/ZF.thy Tue Jun 01 12:33:50 2004 +0200
27.3 @@ -61,7 +61,7 @@
27.4 Pair :: "[i, i] => i"
27.5 fst :: "i => i"
27.6 snd :: "i => i"
27.7 - split :: "[[i, i] => 'a, i] => 'a::logic" --{*for pattern-matching*}
27.8 + split :: "[[i, i] => 'a, i] => 'a::{}" --{*for pattern-matching*}
27.9
27.10 text {*Sigma and Pi Operators *}
27.11 consts