--- a/src/HOL/HOL.thy Tue Apr 23 16:58:57 1996 +0200
+++ b/src/HOL/HOL.thy Tue Apr 23 17:01:51 1996 +0200
@@ -143,40 +143,6 @@
if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
(* start 8bit 1 *)
-types
-('a, 'b) "ë" (infixr 5)
-
-syntax
- "Ú" :: "['a::{}, 'a] => prop" ("(_ Ú/ _)" [3, 2] 2)
- "êë" :: "[prop, prop] => prop" ("(_ êë/ _)" [2, 1] 1)
- "Gbigimpl" :: "[asms, prop] => prop" ("((3Ë _ Ì) êë/ _)" [0, 1] 1)
- "Gall" :: "('a => prop) => prop" (binder "Ä" 0)
-
- "Glam" :: "[idts, 'a::logic] => 'b::logic" ("(3³_./ _)" 10)
- "Û" :: "['a, 'a] => bool" (infixl 50)
- "Gnot" :: "bool => bool" ("¿ _" [40] 40)
- "GEps" :: "[pttrn, bool] => 'a" ("(3®_./ _)" 10)
- "GAll" :: "[idts, bool] => bool" ("(3Â_./ _)" 10)
- "GEx" :: "[idts, bool] => bool" ("(3Ã_./ _)" 10)
- "GEx1" :: "[idts, bool] => bool" ("(3Ã!_./ _)" 10)
- "À" :: "[bool, bool] => bool" (infixr 35)
- "Á" :: "[bool, bool] => bool" (infixr 30)
- "çè" :: "[bool, bool] => bool" (infixr 25)
-
-translations
-(type) "x ë y" == (type) "x => y"
-
-(* "³x.t" => "%x.t" *)
-
- "x Û y" == "x ~= y"
- "¿ y" == "~y"
- "®x.P" == "@x.P"
- "Âx.P" == "! x. P"
- "Ãx.P" == "? x. P"
- "Ã!x.P" == "?! x. P"
- "x À y" == "x & y"
- "x Á y" == "x | y"
- "x çè y" == "x --> y"
(* end 8bit 1 *)
end
@@ -201,36 +167,6 @@
map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
(* start 8bit 2 *)
-local open Ast;
-fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
- fold_ast_p "êë" (unfold_ast "_asms" asms, concl)
- | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
-fun impl_ast_tr' (*"êë"*) asts =
- (case unfold_ast_p "êë" (Appl (Constant "êë" :: asts)) of
- (asms as _ :: _ :: _, concl)
- => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
- | _ => raise Match);
-
-in
-val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr)::
- ("Glam", fn asts => Appl (Constant "_abs" :: asts))::
- parse_ast_translation;
-
-val print_ast_translation = ("êë", impl_ast_tr')::
- ("_lambda", fn asts => Appl (Constant "Glam" :: asts)) ::
- print_ast_translation;
-
-end;
-
-local open Syntax in
-val thy = thy
-|> add_trrules_i
-[mk_appl (Constant "Ú" ) [Variable "P", Variable "Q"] <->
- mk_appl (Constant "==") [Variable "P", Variable "Q"],
- mk_appl (Constant "êë" ) [Variable "P", Variable "Q"] <->
- mk_appl (Constant "==>") [Variable "P", Variable "Q"],
- (Constant "Ä" ) <-> (Constant "!!")]
-end;
(* end 8bit 2 *)