# HG changeset patch
# User oheimb
# Date 838128810 -7200
# Node ID 5b297e9ec3fc356bff4e4d92239f027b6cd4b9af
# Parent 78c4b3ddba6cc31e5eb6ea6b65dd5d8d7a8689b2
unnecessary files removed
diff -r 78c4b3ddba6c -r 5b297e9ec3fc src/Tools/8bit/doc/.Set2g.html
--- a/src/Tools/8bit/doc/.Set2g.html Tue Jul 23 13:19:27 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-Set2g.thy
-
-
-Set2g.thy
-Back to the index of HOL
-
-
-
-Set2g = Ord +
-
-types
- 'a set
-consts
- Ball :: "'a set ë ('a ë bool) ë bool"
-syntax
- "GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
-translations
-(* "ÂxÎA. P" == "Ball A (³x. P)"*)
- "GBall x A P" == "Ball A (³x. P)"
-
-(*defs
-
- Ball_def "Ball A P Ú Âx. xÎA çè P(x)"
-*)
-end
-
-
diff -r 78c4b3ddba6c -r 5b297e9ec3fc src/Tools/8bit/doc/.Set2g.thy.ML
--- a/src/Tools/8bit/doc/.Set2g.thy.ML Tue Jul 23 13:19:27 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-val thy = mk_base [Thy "Ord"] "Set2g" true;
-
-structure Set2g =
-struct
-
-local
- val parse_ast_translation = [];
- val parse_translation = [];
- val print_translation = [];
- val print_ast_translation = [];
-in
-
-
-
-val thy = thy
-
-|> add_trfuns
-(parse_ast_translation, parse_translation, print_translation, print_ast_translation)
-
-|> add_types
-[("set", 1, NoSyn)]
-
-|> add_tyabbrs
-[]
-
-|> add_consts
-[("Ball", "'a set ë ('a ë bool) ë bool", NoSyn)]
-
-|> add_syntax
-[("GBall", "pttrn ë 'a set ë bool ë bool", Mixfix ("(3Â _ Î _ ./ _)", [], 10))]
-
-|> add_trrules
-[("logic", "Â x Î A . P") <-> ("logic", "Ball A (³x. P)")]
-
-|> add_thyname "Set2g";
-
-val _ = store_theory (thy, "Set2g");
-
-
-
-
-end;
-end;
diff -r 78c4b3ddba6c -r 5b297e9ec3fc src/Tools/8bit/doc/.Set2g_sub.html
--- a/src/Tools/8bit/doc/.Set2g_sub.html Tue Jul 23 13:19:27 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-Children of Set2g
-Children of theory Set2g
-The name of every theory is linked to its theory file
-
stands for subtheories (child theories)
-
stands for supertheories (parent theories)
-
-Back to the index of HOL
-
-Set2g
diff -r 78c4b3ddba6c -r 5b297e9ec3fc src/Tools/8bit/doc/.Set2g_sup.html
--- a/src/Tools/8bit/doc/.Set2g_sup.html Tue Jul 23 13:19:27 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-Ancestors of Set2g
-Ancestors of theory Set2g
-The name of every theory is linked to its theory file
- stands for subtheories (child theories)
- stands for supertheories (parent theories)
-
... stands for repeated subtrees
-Back to the index of HOL
-
-Set2g
- \__Ord
- \__HOL
- \__CPure
-
\ No newline at end of file