# HG changeset patch
# User wenzelm
# Date 1003082355 -7200
# Node ID 17a6dcd6f3cf178bf2ac6263592cc4dcd0b17d41
# Parent  9bf11f1de9d67d8d765807e444c3e4513bbe597a
judgment Trueprop;
proper declarations of atomize rules;

diff -r 9bf11f1de9d6 -r 17a6dcd6f3cf src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sat Oct 13 21:46:53 2001 +0200
+++ b/src/FOL/IFOL.thy	Sun Oct 14 19:59:15 2001 +0200
@@ -18,9 +18,10 @@
 
 typedecl o
 
-consts
+judgment
+  Trueprop      :: "o => prop"                  ("(_)" 5)
 
-  Trueprop      :: "o => prop"                  ("(_)" 5)
+consts
   True          :: o
   False         :: o
 
@@ -130,7 +131,7 @@
 
 subsection {* Atomizing meta-level rules *}
 
-lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
+lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
 proof (rule equal_intr_rule)
   assume "!!x. P(x)"
   show "ALL x. P(x)" by (rule allI)
@@ -139,7 +140,7 @@
   thus "!!x. P(x)" by (rule allE)
 qed
 
-lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)"
+lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
 proof (rule equal_intr_rule)
   assume r: "A ==> B"
   show "A --> B" by (rule impI) (rule r)
@@ -148,7 +149,7 @@
   thus B by (rule mp)
 qed
 
-lemma atomize_eq: "(x == y) == Trueprop (x = y)"
+lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
 proof (rule equal_intr_rule)
   assume "x == y"
   show "x = y" by (unfold prems) (rule refl)
@@ -157,7 +158,4 @@
   thus "x == y" by (rule eq_reflection)
 qed
 
-lemmas atomize = atomize_all atomize_imp
-lemmas atomize' = atomize atomize_eq
-
 end