src/HOL/ex/Intuitionistic.thy
changeset 41460 ea56b98aee83
parent 17589 58eeffd73be1
child 58889 5b7a9633cfa8
equal deleted inserted replaced
41441:a7a03f856354 41460:ea56b98aee83
     1 (*  Title:      HOL/ex/Intuitionistic.thy
     1 (*  Title:      HOL/ex/Intuitionistic.thy
     2     ID:         $Id$
       
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     3     Copyright   1991  University of Cambridge
     5 
     4 
     6 Taken from FOL/ex/int.ML
     5 Taken from FOL/ex/int.ML
     7 *)
     6 *)