doc-src/IsarRef/Thy/Base.thy
author wenzelm
Wed, 10 Aug 2011 10:59:37 +0200
changeset 44109 7a44005dc2ec
parent 43564 9864182c6bad
child 48891 c0eafbd55de3
permissions -rw-r--r--
bash_output_fifo blocks on Cygwin 1.7.x;
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