setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
authorwenzelm
Sun May 18 17:03:16 2008 +0200 (2008-05-18)
changeset 269561309a6a0a29f
parent 26955 ebbaa935eae0
child 26957 e3f04fdd994d
setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
src/CTT/CTT.thy
src/Cube/Cube.thy
src/FOL/IFOL.thy
src/FOLP/IFOLP.thy
src/Sequents/Sequents.thy
     1.1 --- a/src/CTT/CTT.thy	Sun May 18 17:03:14 2008 +0200
     1.2 +++ b/src/CTT/CTT.thy	Sun May 18 17:03:16 2008 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4  uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
     1.5  begin
     1.6  
     1.7 +setup PureThy.old_appl_syntax_setup
     1.8 +
     1.9  typedecl i
    1.10  typedecl t
    1.11  typedecl o
     2.1 --- a/src/Cube/Cube.thy	Sun May 18 17:03:14 2008 +0200
     2.2 +++ b/src/Cube/Cube.thy	Sun May 18 17:03:16 2008 +0200
     2.3 @@ -9,6 +9,8 @@
     2.4  imports Pure
     2.5  begin
     2.6  
     2.7 +setup PureThy.old_appl_syntax_setup
     2.8 +
     2.9  typedecl "term"
    2.10  typedecl "context"
    2.11  typedecl typing
     3.1 --- a/src/FOL/IFOL.thy	Sun May 18 17:03:14 2008 +0200
     3.2 +++ b/src/FOL/IFOL.thy	Sun May 18 17:03:16 2008 +0200
     3.3 @@ -26,6 +26,8 @@
     3.4  
     3.5  subsection {* Syntax and axiomatic basis *}
     3.6  
     3.7 +setup PureThy.old_appl_syntax_setup
     3.8 +
     3.9  global
    3.10  
    3.11  classes "term"
     4.1 --- a/src/FOLP/IFOLP.thy	Sun May 18 17:03:14 2008 +0200
     4.2 +++ b/src/FOLP/IFOLP.thy	Sun May 18 17:03:16 2008 +0200
     4.3 @@ -11,6 +11,8 @@
     4.4  uses ("hypsubst.ML") ("intprover.ML")
     4.5  begin
     4.6  
     4.7 +setup PureThy.old_appl_syntax_setup
     4.8 +
     4.9  global
    4.10  
    4.11  classes "term"
     5.1 --- a/src/Sequents/Sequents.thy	Sun May 18 17:03:14 2008 +0200
     5.2 +++ b/src/Sequents/Sequents.thy	Sun May 18 17:03:16 2008 +0200
     5.3 @@ -11,6 +11,8 @@
     5.4  uses ("prover.ML")
     5.5  begin
     5.6  
     5.7 +setup PureThy.old_appl_syntax_setup
     5.8 +
     5.9  declare [[unify_trace_bound = 20, unify_search_bound = 40]]
    5.10  
    5.11  global