(*DOC*)theory iS(*DOC*)
imports Main
begin
section{* FROM: Isabelle2012/etc/symbols *}
subsection{* NOTE: Use a backslash before the "<" in each command. *}
--"However, in jEdit, if you simply start typing what's between '<' and '>',
   the command completion will kick in."
--"Set the SideKick option 'After popup trigger keystroke, wait (seconds)' to
   determine how fast the popup windowd pops up."
subsection{* 0-9 *}
text{*
...\<zero>......<zero>
...\<one>......<one>
...\<two>......<two>
...\<three>......<three>
...\<four>......<four>
...\<five>......<five>
...\<six>......<six>
...\<seven>......<seven>
...\<eight>......<eight>
...\<nine>......<nine>
*}
subsection{* mathcal *}
text{*
...\<A>......<A>
...\<B>......<B>
...\<C>......<C>
...\<D>......<D>
...\<E>......<E>
...\<F>......<F>
...\<G>......<G>
...\<H>......<H>
...\<I>......<I>
...\<J>......<J>
...\<K>......<K>
...\<L>......<L>
...\<M>.....<M>
...\<N>......<N>
...\<O>......<O>
...\<P>......<P>
...\<Q>......<Q>
...\<R>......<R>
...\<S>......<S>
...\<T>......<T>
...\<U>......<U>
...\<V>......<V>
...\<W>.....<W>
...\<X>......<X>
...\<Y>......<Y>
...\<Z>......<Z>
...\<a>......<a>
...\<b>......<b>
...\<c>......<c>
...\<d>......<d>
...\<e>......<e>
...\<f>.......<f>
...\<g>......<g>
...\<h>......<h>
...\<i>.......<i>
...\<j>.......<j>
...\<k>......<k>
...\<l>.......<l>
...\<m>......<m>
...\<n>......<n>
...\<o>......<o>
...\<p>......<p>
...\<q>......<q>
...\<r>......<r>
...\<s>......<s>
...\<t>......<t>
...\<u>......<u>
...\<v>......<v>
...\<w>......<w>
...\<x>......<x>
...\<y>......<y>
...\<z>......<z>
*}
subsection{* mathfrak *}
text{*
...\<AA>......<AA>
...\<BB>.....<BB>
...\<CC>......<CC>
...\<DD>......<DD>
...\<EE>......<EE>
...\<FF>......<FF>
...\<GG>......<GG>
...\<HH>......<HH>
...\<JJ>......<JJ>
...\<KK>......<KK>
...\<LL>......<LL>
...\<MM>.....<MM>
...\<NN>......<NN>
...\<OO>......<OO>
...\<PP>......<PP>
...\<QQ>......<QQ>
...\<SS>......<SS>
...\<TT>......<TT>
...\<UU>......<UU>
...\<VV>......<VV>
...\<WW>.....<WW>
...\<XX>......<XX>
...\<YY>......<YY>
...\<ZZ>......<ZZ>
...\<aa>......<aa>
...\<bb>......<bb>
...\<cc>......<cc>
...\<dd>......<dd>
...\<ee>......<ee>
...\<ff>......<ff>
...\<gg>......<gg>
...\<hh>......<hh>
...\<ii>.......<ii>
...\<jj>.......<jj>
...\<kk>......<kk>
...\<ll>.......<ll>
...\<mm>......<mm>
...\<nn>......<nn>
...\<oo>......<oo>
...\<pp>......<pp>
...\<qq>......<qq>
...\<rr>......<rr>
...\<ss>......<ss>
...\<tt>......<tt>
...\<uu>......<uu>
...\<vv>......<vv>
...\<ww>......<ww>
...\<xx>......<xx>
...\<yy>......<yy>
...\<zz>......<zz>
*}
subsection{* Greek *}
text{*
...\<alpha>......<alpha>
...\<beta>......<beta>
...\<gamma>......<gamma>
...\<delta>......<delta>
...\<epsilon>......<epsilon>
...\<zeta>......<zeta>
...\<eta>......<eta>
...\<theta>......<theta>
...\<iota>......<iota>
...\<kappa>......<kappa>
...\<lambda>......<lambda>               abbrev: %
...\<mu>......<mu>
...\<nu>......<nu>
...\<xi>......<xi>
...\<pi>......<pi>
...\<rho>......<rho>
...\<sigma>......<sigma>
...\<tau>......<tau>
...\<upsilon>......<upsilon>
...\<phi>......<phi>
...\<chi>......<chi>
...\<psi>......<psi>
...\<omega>......<omega>
...\<Gamma>......<Gamma>
...\<Delta>......<Delta>
...\<Theta>......<Theta>
...\<Lambda>......<Lambda>
...\<Xi>......<Xi>
...\<Pi>......<Pi>
...\<Sigma>......<Sigma>
...\<Upsilon>......<Upsilon>
...\<Phi>......<Phi>
...\<Psi>......<Psi>
...\<Omega>......<Omega>
*}
subsection{* Blackboard Bold *}
text{*
...\<bool>......<bool>
...\<complex>......<complex>
...\<nat>......<nat>
...\<rat>......<rat>
...\<real>......<real>
...\<int>......<int>
*}
subsection{* Arrows, Etc. *}
text{*
...\<leftarrow>.....<leftarrow>
...\<longleftarrow>....<longleftarrow>
...\<rightarrow>.....<rightarrow>           abbrev: ->
...\<longrightarrow>....<longrightarrow>       abbrev: -->
...\<Leftarrow>.....<Leftarrow>
...\<Longleftarrow>....<Longleftarrow>
...\<Rightarrow>.....<Rightarrow>           abbrev: =>
...\<Longrightarrow>....<Longrightarrow>       abbrev: ==>
...\<leftrightarrow>.....<leftrightarrow>
...\<longleftrightarrow>....<longleftrightarrow>   abbrev: <->
...\<Leftrightarrow>.....<Leftrightarrow>
...\<Longleftrightarrow>....<Longleftrightarrow>   abbrev: <=>
...\<mapsto>.....<mapsto>               abbrev: |->
...\<longmapsto>....<longmapsto>           abbrev: |-->
...\<midarrow>......<midarrow>
...\<Midarrow>......<Midarrow>
...\<hookleftarrow>.....<hookleftarrow>
...\<hookrightarrow>.....<hookrightarrow>
...\<leftharpoondown>.....<leftharpoondown>
...\<rightharpoondown>.....<rightharpoondown>
...\<leftharpoonup>.....<leftharpoonup>
...\<rightharpoonup>.....<rightharpoonup>
...\<rightleftharpoons>.....<rightleftharpoons>
...\<leadsto>.....<leadsto>              abbrev: ~>
...\<downharpoonleft>......<downharpoonleft>
...\<downharpoonright>......<downharpoonright>
...\<upharpoonleft>......<upharpoonleft>
...\<restriction>......<restriction>
...\<Colon>......<Colon>
...\<up>......<up>
...\<Up>......<Up>
...\<down>......<down>
...\<Down>......<Down>
...\<updown>......<updown>
...\<Updown>......<Updown>
*}
subsection{* Delimiters *}
text{*
...\<langle>......<langle>               abbrev: <.
...\<rangle>......<rangle>               abbrev: .>
...\<lceil>......<lceil>
...\<rceil>......<rceil>
...\<lfloor>......<lfloor>
...\<rfloor>......<rfloor>
...\<lparr>......<lparr>                abbrev: (|
...\<rparr>......<rparr>                abbrev: |)
...\<lbrakk>......<lbrakk>               abbrev: [|
...\<rbrakk>......<rbrakk>               abbrev: |]
...\<lbrace>......<lbrace>               abbrev: {.
...\<rbrace>......<rbrace>               abbrev: .}
...\<guillemotleft>......<guillemotleft>        abbrev: <<
...\<guillemotright>......<guillemotright>       abbrev: >>
*}
subsection{* Logic, Etc. *}
text{*
...\<bottom>......<bottom>
...\<top>......<top>
...\<and>......<and>                  abbrev: /\, &
...\<And>......<And>                  abbrev: !!
...\<or>......<or>                   abbrev: \/, |
...\<Or>.....<Or>                    abbrev: ??
...\<forall>......<forall>               abbrev: !, ALL
...\<exists>......<exists>               abbrev: ?, EX
...\<nexists>......<nexists>              abbrev: ~?
...\<not>......<not>                  abbrev: ~
...\<box>......<box>
...\<diamond>......<diamond>
...\<turnstile>......<turnstile>            abbrev: |-
...\<Turnstile>.....<Turnstile>             abbrev: |=
...\<tturnstile>......<tturnstile>           abbrev: ||-
...\<TTurnstile>.....<TTurnstile>           abbrev: ||=
...\<stileturn>......<stileturn>            abbrev: -|
*}
subsection{* Relations, Etc. *}
text{*
...\<surd>......<surd>
...\<le>......<le>                   abbrev: <=
...\<ge>......<ge>                   abbrev: >=
...\<lless>.....<lless>
...\<ggreater>.....<ggreater>
...\<lesssim>......<lesssim>
...\<greatersim>......<greatersim>
...\<lessapprox>......<lessapprox>
...\<greaterapprox>......<greaterapprox>
*}
subsection{* Sets *}
text{*
...\<in>......<in>                   abbrev: :
...\<notin>......<notin>                abbrev: ~:
...\<subset>......<subset>
...\<supset>......<supset>
...\<subseteq>......<subseteq>             abbrev: (=
...\<supseteq>......<supseteq>             abbrev: =)
...\<sqsubset>......<sqsubset>
...\<sqsupset>......<sqsupset>
...\<sqsubseteq>......<sqsubseteq>           abbrev: [=
...\<sqsupseteq>......<sqsupseteq>           abbrev: =]
...\<inter>......<inter>                abbrev: Int
...\<Inter>......<Inter>                abbrev: Inter
...\<union>......<union>                abbrev: Un
...\<Union>......<Union>                abbrev: Union
...\<squnion>......<squnion>
...\<Squnion>......<Squnion>
...\<sqinter>......<sqinter>
...\<Sqinter>......<Sqinter>
...\<setminus>......<setminus>
...\<propto>......<propto>
...\<uplus>......<uplus>
...\<Uplus>......<Uplus>
*}
subsection{* Relations, Etc. *}
text{*
...\<noteq>......<noteq>                abbrev: ~=
...\<sim>......<sim>
...\<doteq>......<doteq>
...\<simeq>......<simeq>
...\<approx>......<approx>
...\<asymp>......<asymp>
...\<cong>......<cong>
...\<smile>......<smile>
...\<equiv>......<equiv>                abbrev: ==
...\<frown>.....<frown>
...\<Join>......<Join>
...\<bowtie>......<bowtie>
...\<prec>......<prec>
...\<succ>......<succ>
...\<preceq>......<preceq>
...\<succeq>......<succeq>
...\<parallel>......<parallel>             abbrev: ||
*}
subsection{* Operators, Etc. *}
text{*
...\<bar>......<bar>
...\<plusminus>......<plusminus>
...\<minusplus>......<minusplus>
...\<times>......<times>
...\<div>......<div>
...\<cdot>......<cdot>
...\<star>......<star>
...\<bullet>......<bullet>
...\<circ>......<circ>
...\<dagger>......<dagger>
...\<ddagger>......<ddagger>
...\<lhd>......<lhd>
...\<rhd>......<rhd>
...\<unlhd>......<unlhd>
...\<unrhd>......<unrhd>
...\<triangleleft>......<triangleleft>
...\<triangleright>......<triangleright>
...\<triangle>......<triangle>
...\<triangleq>......<triangleq>
...\<oplus>......<oplus>                abbrev: +o
...\<Oplus>.....<Oplus>                abbrev: +O
...\<otimes>......<otimes>               abbrev: *o
...\<Otimes>.....<Otimes>               abbrev: *O
...\<odot>......<odot>                 abbrev: .o
...\<Odot>.....<Odot>                 abbrev: .O
...\<ominus>......<ominus>               abbrev: -o
...\<oslash>......<oslash>               abbrev: /o
...\<dots>.....<dots>                 abbrev: ...
...\<cdots>.....<cdots>
...\<Sum>.....<Sum>                  abbrev: SUM
...\<Prod>.....<Prod>                 abbrev: PROD
...\<Coprod>.....<Coprod>
...\<infinity>.....<infinity>
...\<integral>......<integral>
...\<ointegral>......<ointegral>
...\<clubsuit>......<clubsuit>
...\<diamondsuit>......<diamondsuit>
...\<heartsuit>......<heartsuit>
...\<spadesuit>......<spadesuit>
...\<aleph>......<aleph>
...\<emptyset>......<emptyset>
...\<nabla>......<nabla>
...\<partial>......<partial>
...\<Re>......<Re>
...\<Im>......<Im>
*}
subsection{* Symbols, Etc. *}
text{*
...\<flat>......<flat>
...\<natural>......<natural>
...\<sharp>......<sharp>
...\<angle>......<angle>
...\<copyright>......<copyright>
...\<registered>......<registered>
...\<hyphen>......<hyphen>
...\<inverse>......<inverse>
...\<onesuperior>......<onesuperior>
...\<onequarter>......<onequarter>
...\<twosuperior>......<twosuperior>
...\<onehalf>......<onehalf>
...\<threesuperior>......<threesuperior>
...\<threequarters>......<threequarters>
...\<ordfeminine>......<ordfeminine>
...\<ordmasculine>......<ordmasculine>
...\<section>......<section>
...\<paragraph>......<paragraph>
...\<exclamdown>......<exclamdown>
...\<questiondown>......<questiondown>
...\<euro>......<euro>
...\<pounds>......<pounds>
...\<yen>......<yen>
...\<cent>......<cent>
...\<currency>......<currency>
...\<degree>......<degree>
...\<amalg>......<amalg>
...\<mho>......<mho>
...\<lozenge>......<lozenge>
...\<wp>......<wp>
...\<wrong>.......<wrong>
...\<struct>......<struct>
...\<acute>......<acute>
...\<index>......<index>
...\<dieresis>......<dieresis>
...\<cedilla>......<cedilla>
...\<hungarumlaut>......<hungarumlaut>
...\<some>......<some>
*}
subsection{* Subscripts & Superscripts *}
text{*
...\<^sub>.......<^sub>                 abbrev: =_
...\<^sup>.......<^sup>                 abbrev: =^
...\<^isub>.......<^isub>                abbrev: -_
...\<^isup>.......<^isup>                abbrev: -^
...\<^bsub>......<^bsub>                abbrev: =_(
...\<^esub>......<^esub>                abbrev: =_)
...\<^bsup>......<^bsup>                abbrev: =^(
...\<^esup>......<^esup>                abbrev: =^)
...\<^bold>.......<^bold>                abbrev: -.
*}

section{* OPERATOR PRIORITY: 2012 HOL *}
--{*                                                                   02ho = src/HOL.thy                           *}
--{*       PRIORITY                                                    FILE-LINE                       WHY INTRODUCED
           __01__                                             *}--{*-----------------------------------
=simp=...................[prop, prop] => prop..........................02ho 1843 (infixr "=simp=>" 1)  definition
           __05__                                             *}--{*-----------------------------------
Trueprop.................bool => prop..................................02ho 0067 ("(_)" 5)             judgment
If.......................bool => 'a => 'a => 'a........................02ho 0189 ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)   definition
           __10__                                             *}--{*-----------------------------------
_bind....................[pttrn, 'a] => letbind........................02ho 0129 ("(2_ =/ _)" 10)      syntax
_case_syntax.............['a, cases_syn] => 'b.........................02ho 0136 ("(case _ of/ _)" 10) syntax
_case1...................['a, 'b] => case_syn..........................02ho 0137 ("(2_ =>/ _)" 10)     syntax
                                                                       02ho 0141 ("(2_ \<Rightarrow>/ _)" 10)     xsymbols
_Let.....................[letbinds, 'a] => 'a..........................02ho 0132 ("(let (_)/ in (_))" [0, 10] 10)   syntax
_The.....................[pttrn, bool] => 'a...........................02ho 0119 ("(3THE _./ _)" [0, 10] 10)        syntax
All......................('a => bool) => bool..........................02ho 0082 (binder "ALL " 10)    consts
                                                                       02ho 0144 (binder "\<forall>" 10)       xsymbols
                                                                       02ho 0149 (binder "\<forall>" 10)       HTML
                                                                       02ho 0154 (binder "! " 10)      HOL
Ex.......................('a => bool) => bool..........................02ho 0083 (binder "EX " 10)     consts
                                                                       02ho 0145 (binder "\<exists>" 10)       xsymbols
                                                                       02ho 0150 (binder "\<exists>" 10)       HTML
                                                                       02ho 0155 (binder "? " 10)      HOL
Ex1......................('a => bool) => bool..........................02ho 0084 (binder "EX! " 10)    consts
                                                                       02ho 0146 (binder "\<exists>!" 10)      xsymbols
                                                                       02ho 0151 (binder "\<exists>!" 10)      HTML
                                                                       02ho 0156 (binder "?! " 10)     HOL
           __25__                                             *}--{*-----------------------------------
implies..................[bool, bool] => bool..........................02ho 0070 (infixr "-->" 25)     axiomatization
                                                                       02ho 0103 (infixr "\<longrightarrow>" 25)     xsymbols
iff......................[bool, bool] => bool..........................02ho 0113 (infixr "<->" 25)     abbreviation
                                                                       02ho 0117 (infixr "\<longleftrightarrow>" 25)     xsymbols
           __30__                                             *}--{*-----------------------------------
disj.....................[bool, bool] => bool..........................02ho 0080 (infixr "|" 30)      consts
                                                                       02ho 0102 (infixr "\<or>" 30)      xsymbols
                                                                       02ho 0109 (infixr "\<or>" 30)      HTML
           __35__                                             *}--{*-----------------------------------
conj.....................[bool, bool] => bool..........................02ho 0079 (infixr "&" 35)      consts
                                                                       02ho 0101 (infixr "\<and>" 35)      xsymbols
                                                                       02ho 0108 (infixr "\<and>" 35)      HTML
           __40__                                             *}--{*-----------------------------------
Not......................bool => bool..................................02ho 0077 ("~ _" [40] 40)      consts
                                                                       02ho 0100 ("\<not> _" [40] 40)      xsymbols
                                                                       02ho 0107 ("\<not> _" [40] 40)      HTML
           __50__                                             *}--{*-----------------------------------
eq.......................['a, 'a] => bool..............................02ho 0071 (infixl "=" 50)      axiomatization
                                                                       02ho 0090 (infix "=" 50)       output
not_equal................['a, 'a] => bool..............................02ho 0093 (infixl "~=" 50)     abbreviation
                                                                       02ho 0097 (infix "~=" 50)      output
                                                                       02ho 0104 (infix "\<noteq>" 50)       xsymbols
                                                                       02ho 0110 (infix "\<noteq>" 50)       HTML
*}

section{* PRIORITY: 2012 PURE *}
text{* From ~~/src/Pure/pure_thy.ML

(*  Title:      Pure/pure_thy.ML
    Author:     Markus Wenzel, TU Muenchen

Pure theory syntax and further logical content.
*)

signature PURE_THY =
sig
  val old_appl_syntax: theory -> bool
  val old_appl_syntax_setup: theory -> theory
end;

structure Pure_Thy: PURE_THY =
struct

val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;

val tycon = Lexicon.mark_type;
val const = Lexicon.mark_const;


(* application syntax variants *)

val appl_syntax =
 [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
  ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];

val applC_syntax =
 [("",       typ "'a => cargs",                  Delimfix "_"),
  ("_cargs", typ "'a => cargs => cargs",         Mixfix ("_/ _", [1000, 1000], 1000)),
  ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
  ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];

structure Old_Appl_Syntax = Theory_Data
(
  type T = bool;
  val empty = false;
  val extend = I;
  fun merge (b1, b2) : T =
    if b1 = b2 then b1
    else error "Cannot merge theories with different application syntax";
);

val old_appl_syntax = Old_Appl_Syntax.get;

val old_appl_syntax_setup =
  Old_Appl_Syntax.put true #>
  Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
  Sign.add_syntax_i appl_syntax;


(* main content *)

val _ = Context.>> (Context.map_theory
  (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
   Old_Appl_Syntax.put false #>
   Sign.add_types_global
   [(Binding.name "fun", 2, NoSyn),
    (Binding.name "prop", 0, NoSyn),
    (Binding.name "itself", 1, NoSyn),
    (Binding.name "dummy", 0, NoSyn)]
  #> Sign.add_nonterminals_global (map Binding.name Syntax.basic_nonterms)
  #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
  #> Sign.add_syntax_i
   [("",            typ "prop' => prop",               Delimfix "_"),
    ("",            typ "logic => any",                Delimfix "_"),
    ("",            typ "prop' => any",                Delimfix "_"),
    ("",            typ "logic => logic",              Delimfix "'(_')"),
    ("",            typ "prop' => prop'",              Delimfix "'(_')"),
    ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
    ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
    ("",            typ "tid => type",                 Delimfix "_"),
    ("",            typ "tvar => type",                Delimfix "_"),
    ("",            typ "type_name => type",           Delimfix "_"),
    ("_type_name",  typ "id => type_name",             Delimfix "_"),
    ("_type_name",  typ "longid => type_name",         Delimfix "_"),
    ("_ofsort",     typ "tid => sort => type",         Mixfix ("_::_", [1000, 0], 1000)),
    ("_ofsort",     typ "tvar => sort => type",        Mixfix ("_::_", [1000, 0], 1000)),
    ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], 1000)),
    ("",            typ "class_name => sort",          Delimfix "_"),
    ("_class_name", typ "id => class_name",            Delimfix "_"),
    ("_class_name", typ "longid => class_name",        Delimfix "_"),
    ("_topsort",    typ "sort",                        Delimfix "{}"),
    ("_sort",       typ "classes => sort",             Delimfix "{_}"),
    ("",            typ "class_name => classes",       Delimfix "_"),
    ("_classes",    typ "class_name => classes => classes", Delimfix "_,_"),
    ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [1000, 0], 1000)),
    ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
    ("",            typ "type => types",               Delimfix "_"),
    ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ => _)", [1, 0], 0)),
    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ => _)", [0, 0], 0)),
    ("",            typ "type => type",                Delimfix "'(_')"),
    ("\\<^type>dummy", typ "type",                     Delimfix "'_"),
    ("_type_prop",  typ "'a",                          NoSyn),
    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
    ("_abs",        typ "'a",                          NoSyn),
    ("",            typ "'a => args",                  Delimfix "_"),
    ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
    ("",            typ "id_position => idt",          Delimfix "_"),
    ("_idtdummy",   typ "idt",                         Delimfix "'_"),
    ("_idtyp",      typ "id_position => type => idt",  Mixfix ("_::_", [], 0)),
    ("_idtypdummy", typ "type => idt",                 Mixfix ("'_()::_", [], 0)),
    ("",            typ "idt => idt",                  Delimfix "'(_')"),
    ("",            typ "idt => idts",                 Delimfix "_"),
    ("_idts",       typ "idt => idts => idts",         Mixfix ("_/ _", [1, 0], 0)),
    ("",            typ "idt => pttrn",                Delimfix "_"),
    ("",            typ "pttrn => pttrns",             Delimfix "_"),
    ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
    ("",            typ "aprop => aprop",              Delimfix "'(_')"),
    ("",            typ "id_position => aprop",        Delimfix "_"),
    ("",            typ "longid_position => aprop",    Delimfix "_"),
    ("",            typ "var => aprop",                Delimfix "_"),
    ("_DDDOT",      typ "aprop",                       Delimfix "..."),
    ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
    ("_asm",        typ "prop => asms",                Delimfix "_"),
    ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
    ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    ("_mk_ofclass", typ "dummy",                       NoSyn),
    ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
    ("",            typ "id_position => logic",        Delimfix "_"),
    ("",            typ "longid_position => logic",    Delimfix "_"),
    ("",            typ "var => logic",                Delimfix "_"),
    ("_DDDOT",      typ "logic",                       Delimfix "..."),
    ("_strip_positions", typ "'a", NoSyn),
    ("_position",   typ "num_token => num_position",   Delimfix "_"),
    ("_position",   typ "float_token => float_position", Delimfix "_"),
    ("_position",   typ "xnum_token => xnum_position", Delimfix "_"),
    ("_constify",   typ "num_position => num_const",   Delimfix "_"),
    ("_constify",   typ "float_position => float_const", Delimfix "_"),
    ("_constify",   typ "xnum_position => xnum_const", Delimfix "_"),
    ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    ("_indexdefault", typ "index",                     Delimfix ""),
    ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
    ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
    ("_update_name", typ "idt",                        NoSyn),
    ("_constrainAbs", typ "'a",                        NoSyn),
    ("_position",   typ "id => id_position",           Delimfix "_"),
    ("_position",   typ "longid => longid_position",   Delimfix "_"),
    ("_position",   typ "str_token => str_position",   Delimfix "_"),
    ("_type_constraint_", typ "'a",                    NoSyn),
    ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
    ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
    ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
    ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
    ("_context_xconst", typ "id_position => logic",    Delimfix "XCONST _"),
    ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
    ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
    ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
    (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
    (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
    ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
    (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
    (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
  #> Sign.add_syntax_i applC_syntax
  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    ("_ofsort",           typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
    ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    ("_constrain",        typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
    ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    (const "==",          typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
    (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
    ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
  #> Sign.add_modesyntax_i ("", false)
   [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
  #> Sign.add_modesyntax_i ("HTML", false)
   [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
  #> Sign.add_consts_i
   [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
    (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    (Binding.name "prop", typ "prop => prop", NoSyn),
    (Binding.name "TYPE", typ "'a itself", NoSyn),
    (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
  #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
  #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
  #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
  #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
  #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
  #> Sign.add_trfuns Syntax_Trans.pure_trfuns
  #> Sign.local_path
  #> Sign.add_consts_i
   [(Binding.name "term", typ "'a => prop", NoSyn),
    (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
    (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
  #> (Global_Theory.add_defs false o map Thm.no_attributes)
   [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
    (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
    (Binding.name "sort_constraint_def",
      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
      \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
    (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
  #> Sign.hide_const false "Pure.term"
  #> Sign.hide_const false "Pure.sort_constraint"
  #> Sign.hide_const false "Pure.conjunction"
  #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
  #> fold (fn (a, prop) =>
      snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));

end;

*}

end