doc-src/IsarRef/Thy/Base.thy
author huffman
Thu, 08 Sep 2011 19:35:23 -0700
changeset 44849 41fddafe20d5
parent 43564 9864182c6bad
child 48891 c0eafbd55de3
permissions -rw-r--r--
Library/Saturated.thy: number_semiring class instance
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42651
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
     1
theory Base
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
     2
imports Pure
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
     3
uses "../../antiquote_setup.ML"
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
     4
begin
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
     5
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
     6
setup {*
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42651
diff changeset
     7
  Antiquote_Setup.setup #>
42651
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
     8
  member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
     9
*}
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
    10
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
    11
declare [[thy_output_source]]
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
    12
e3fdb7c96be5 formal Base theory;
wenzelm
parents:
diff changeset
    13
end