expose formal text;
authorwenzelm
Sun Mar 14 14:29:30 2010 +0100 (2010-03-14)
changeset 35787afdf1c4958b2
parent 35786 9d8cd1ca8c61
child 35788 f1deaca15ca3
expose formal text;
src/HOL/Library/Lattice_Syntax.thy
src/HOL/Library/Quotient_Syntax.thy
     1.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Sun Mar 14 14:10:21 2010 +0100
     1.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Sun Mar 14 14:29:30 2010 +0100
     1.3 @@ -2,7 +2,6 @@
     1.4  
     1.5  header {* Pretty syntax for lattice operations *}
     1.6  
     1.7 -(*<*)
     1.8  theory Lattice_Syntax
     1.9  imports Complete_Lattice
    1.10  begin
    1.11 @@ -16,4 +15,3 @@
    1.12    Sup  ("\<Squnion>_" [900] 900)
    1.13  
    1.14  end
    1.15 -(*>*)
    1.16 \ No newline at end of file
     2.1 --- a/src/HOL/Library/Quotient_Syntax.thy	Sun Mar 14 14:10:21 2010 +0100
     2.2 +++ b/src/HOL/Library/Quotient_Syntax.thy	Sun Mar 14 14:29:30 2010 +0100
     2.3 @@ -1,10 +1,9 @@
     2.4 -(*  Title:      Quotient_Syntax.thy
     2.5 +(*  Title:      HOL/Library/Quotient_Syntax.thy
     2.6      Author:     Cezary Kaliszyk and Christian Urban
     2.7  *)
     2.8  
     2.9  header {* Pretty syntax for Quotient operations *}
    2.10  
    2.11 -(*<*)
    2.12  theory Quotient_Syntax
    2.13  imports Main
    2.14  begin
    2.15 @@ -15,4 +14,3 @@
    2.16    fun_rel (infixr "===>" 55)
    2.17  
    2.18  end
    2.19 -(*>*)