src/LCF/ex/Ex4.thy
author paulson
Thu, 18 Jul 2002 10:37:55 +0200
changeset 13387 b7464ca2ebbb
parent 4905 be73ddff6c5a
child 17248 81bf91654e73
permissions -rw-r--r--
new theorems to support Constructible proofs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4905
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
     1
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
     2
(*** Prefixpoints ***)
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
     3
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
     4
Ex4 = LCF