src/Pure/Pure.thy
changeset 27681 8cedebf55539
parent 26958 ed3a58a9eae1
child 28699 32b6a8f12c1c
     1.1 --- a/src/Pure/Pure.thy	Fri Jul 25 12:03:31 2008 +0200
     1.2 +++ b/src/Pure/Pure.thy	Fri Jul 25 12:03:32 2008 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  subsection {* Embedded terms *}
     1.6  
     1.7 -locale (open) meta_term_syntax =
     1.8 +locale meta_term_syntax =
     1.9    fixes meta_term :: "'a => prop"  ("TERM _")
    1.10  
    1.11  lemmas [intro?] = termI
    1.12 @@ -34,7 +34,7 @@
    1.13  
    1.14  subsection {* Meta-level conjunction *}
    1.15  
    1.16 -locale (open) meta_conjunction_syntax =
    1.17 +locale meta_conjunction_syntax =
    1.18    fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.19  
    1.20  lemma all_conjunction: