1.1 --- a/doc-src/IsarRef/Thy/Synopsis.thy	Tue May 31 22:47:18 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Synopsis.thy	Wed Jun 01 12:20:48 2011 +0200
     1.3 @@ -8,10 +8,33 @@
     1.4  
     1.5  text {*
     1.6    An Isar proof body serves as mathematical notepad to compose logical
     1.7 -  content, consisting of facts, terms, types.
     1.8 +  content, consisting of types, terms, facts.
     1.9  *}
    1.10  
    1.11  
    1.12 +subsection {* Types and terms *}
    1.13 +
    1.14 +notepad
    1.15 +begin
    1.16 +  txt {* Locally fixed entities: *}
    1.17 +  fix x   -- {* local constant, without any type information yet *}
    1.18 +  fix x :: 'a  -- {* variant with explicit type-constraint for subsequent use*}
    1.19 +
    1.20 +  fix a b
    1.21 +  assume "a = b"  -- {* type assignment at first occurrence in concrete term *}
    1.22 +
    1.23 +  txt {* Definitions (non-polymorphic): *}
    1.24 +  def x \<equiv> "t::'a"
    1.25 +
    1.26 +  txt {* Abbreviations (polymorphic): *}
    1.27 +  let ?f = "\<lambda>x. x"
    1.28 +  term "?f ?f"
    1.29 +
    1.30 +  txt {* Notation: *}
    1.31 +  write x  ("***")
    1.32 +end
    1.33 +
    1.34 +
    1.35  subsection {* Facts *}
    1.36  
    1.37  text {*
    1.38 @@ -190,27 +213,4 @@
    1.39  
    1.40  end
    1.41  
    1.42 -
    1.43 -subsection {* Terms and Types *}
    1.44 -
    1.45 -notepad
    1.46 -begin
    1.47 -  txt {* Locally fixed entities: *}
    1.48 -  fix x   -- {* local constant, without any type information yet *}
    1.49 -  fix x :: 'a  -- {* variant with explicit type-constraint for subsequent use*}
    1.50 -
    1.51 -  fix a b
    1.52 -  assume "a = b"  -- {* type assignment at first occurrence in concrete term *}
    1.53 -
    1.54 -  txt {* Definitions (non-polymorphic): *}
    1.55 -  def x \<equiv> "t::'a"
    1.56 -
    1.57 -  txt {* Abbreviations (polymorphic): *}
    1.58 -  let ?f = "\<lambda>x. x"
    1.59 -  term "?f ?f"
    1.60 -
    1.61 -  txt {* Notation: *}
    1.62 -  write x  ("***")
    1.63 -end
    1.64 -
    1.65  end
    1.66 \ No newline at end of file