doc-src/IsarRef/Thy/Base.thy
author wenzelm
Wed, 30 Nov 2011 23:30:08 +0100
changeset 45701 615da8b8d758
parent 43564 9864182c6bad
child 48891 c0eafbd55de3
permissions -rw-r--r--
discontinued obsolete datatype "alt_names";
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