src/Pure/Isar/local_defs.ML
changeset 18896 efd9d44a0bdb
parent 18875 853fa34047a4
child 18950 053e830c25ad
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Feb 02 12:52:20 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Feb 02 12:52:21 2006 +0100
     1.3 @@ -90,12 +90,11 @@
     1.4    |> Thm.cterm_of (Thm.theory_of_cterm cprop);
     1.5  
     1.6  (*
     1.7 -  [x]
     1.8 -  [x == t]
     1.9 -     :
    1.10 -    B x
    1.11 -  --------
    1.12 -    B t
    1.13 +  [x, x == t]
    1.14 +       :
    1.15 +      B x
    1.16 +  -----------
    1.17 +      B t
    1.18  *)
    1.19  fun def_export _ cprops thm =
    1.20    thm