src/HOL/Recdef.thy
changeset 12023 d982f98e0f0d
parent 11533 0c0d2332e8f0
child 12437 6d4e02b6dd43
     1.1 --- a/src/HOL/Recdef.thy	Sat Nov 03 01:33:33 2001 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Sat Nov 03 01:33:54 2001 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4  (*  Title:      HOL/Recdef.thy
     1.5      ID:         $Id$
     1.6      Author:     Konrad Slind and Markus Wenzel, TU Muenchen
     1.7 +*)
     1.8  
     1.9 -TFL: recursive function definitions.
    1.10 -*)
    1.11 +header {* TFL: recursive function definitions *}
    1.12  
    1.13  theory Recdef = Wellfounded_Relations + Datatype
    1.14  files
    1.15 @@ -34,13 +34,13 @@
    1.16  lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
    1.17    by blast
    1.18  
    1.19 -lemma tfl_disj_assoc: "(a \\<or> b) \\<or> c == a \\<or> (b \\<or> c)"
    1.20 +lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
    1.21    by simp
    1.22  
    1.23 -lemma tfl_disjE: "P \\<or> Q ==> P --> R ==> Q --> R ==> R"
    1.24 +lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
    1.25    by blast
    1.26  
    1.27 -lemma tfl_exE: "\\<exists>x. P x ==> \\<forall>x. P x --> Q ==> Q"
    1.28 +lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    1.29    by blast
    1.30  
    1.31  use "../TFL/utils.ML"