src/Pure/assumption.ML
changeset 67721 5348bea4accd
parent 59150 71b416020f42
child 70313 9c19e15c8548
     1.1 --- a/src/Pure/assumption.ML	Sun Feb 25 12:59:08 2018 +0100
     1.2 +++ b/src/Pure/assumption.ML	Sun Feb 25 15:44:46 2018 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4       :
     1.5       B
     1.6    --------
     1.7 -  #A ==> B
     1.8 +  #A \<Longrightarrow> B
     1.9  *)
    1.10  fun assume_export is_goal asms =
    1.11    (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t);
    1.12 @@ -44,7 +44,7 @@
    1.13       :
    1.14       B
    1.15    -------
    1.16 -  A ==> B
    1.17 +  A \<Longrightarrow> B
    1.18  *)
    1.19  fun presume_export _ = assume_export false;
    1.20  
    1.21 @@ -60,7 +60,7 @@
    1.22  (** local context data **)
    1.23  
    1.24  datatype data = Data of
    1.25 - {assms: (export * cterm list) list,    (*assumes: A ==> _*)
    1.26 + {assms: (export * cterm list) list,    (*assumes: A \<Longrightarrow> _*)
    1.27    prems: thm list};                     (*prems: A |- norm_hhf A*)
    1.28  
    1.29  fun make_data (assms, prems) = Data {assms = assms, prems = prems};