doc-src/IsarRef/Thy/Base.thy
author blanchet
Sun, 04 Mar 2012 23:20:43 +0100
changeset 46818 2a28e66e2e4c
parent 43564 9864182c6bad
child 48891 c0eafbd55de3
permissions -rw-r--r--
ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
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