--- a/src/CTT/Bool.thy Fri Sep 16 21:02:15 2005 +0200
+++ b/src/CTT/Bool.thy Fri Sep 16 23:01:29 2005 +0200
@@ -2,18 +2,26 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-
-The two-element type (booleans and conditionals)
*)
-Bool = CTT +
+header {* The two-element type (booleans and conditionals) *}
+
+theory Bool
+imports CTT
+uses "~~/src/Provers/typedsimp.ML" "rew.ML"
+begin
-consts Bool :: "t"
- true,false :: "i"
- cond :: "[i,i,i]=>i"
-rules
- Bool_def "Bool == T+T"
- true_def "true == inl(tt)"
- false_def "false == inr(tt)"
- cond_def "cond(a,b,c) == when(a, %u. b, %u. c)"
+consts
+ Bool :: "t"
+ true :: "i"
+ false :: "i"
+ cond :: "[i,i,i]=>i"
+defs
+ Bool_def: "Bool == T+T"
+ true_def: "true == inl(tt)"
+ false_def: "false == inr(tt)"
+ cond_def: "cond(a,b,c) == when(a, %u. b, %u. c)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end