src/Doc/Isar_Ref/Proof.thy
changeset 67119 acb0807ddb56
parent 64926 75ee8475c37e
child 69597 ff784d5a5bfb
     1.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sun Dec 03 13:22:09 2017 +0100
     1.3 @@ -128,7 +128,6 @@
     1.4      @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     1.5      @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     1.6      @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     1.7 -    @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     1.8    \end{matharray}
     1.9  
    1.10    The logical proof context consists of fixed variables and assumptions. The
    1.11 @@ -169,11 +168,6 @@
    1.12      ;
    1.13      @@{command define} @{syntax vars} @'where'
    1.14        (@{syntax props} + @'and') @{syntax for_fixes}
    1.15 -    ;
    1.16 -    @@{command def} (def + @'and')
    1.17 -    ;
    1.18 -    def: @{syntax thmdecl}? \<newline>
    1.19 -      @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
    1.20    \<close>}
    1.21  
    1.22    \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary,
    1.23 @@ -207,9 +201,6 @@
    1.24    \<^medskip>
    1.25    It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f
    1.26    :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>.
    1.27 -
    1.28 -  \<^descr> \<^theory_text>\<open>def x \<equiv> t\<close> introduces a local (non-polymorphic) definition. This is an
    1.29 -  old form of \<^theory_text>\<open>define x where "x = t"\<close>.
    1.30  \<close>
    1.31  
    1.32