src/HOL/HOL.thy
changeset 1674 33aff4d854e4
parent 1672 2c109cd2fdd0
child 2260 b59781f2b809
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 23 16:58:57 1996 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 23 17:01:51 1996 +0200
     1.3 @@ -143,40 +143,6 @@
     1.4    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
     1.5  
     1.6  (* start 8bit 1 *)
     1.7 -types
     1.8 -('a, 'b) ""          (infixr 5)
     1.9 -
    1.10 -syntax
    1.11 -  ""		:: "['a::{}, 'a] => prop"       ("(_ / _)"         [3, 2] 2)
    1.12 -  ""		:: "[prop, prop] => prop"	("(_ / _)"        [2, 1] 1)
    1.13 -  "Gbigimpl"	:: "[asms, prop] => prop"	("((3 _ ) / _)" [0, 1] 1)
    1.14 -  "Gall"	:: "('a => prop) => prop"	(binder ""                0)
    1.15 -
    1.16 -  "Glam"         :: "[idts, 'a::logic] => 'b::logic"  ("(3_./ _)" 10)
    1.17 -  ""           :: "['a, 'a] => bool"                 (infixl 50)
    1.18 -  "Gnot"        :: "bool => bool"                     (" _" [40] 40)
    1.19 -  "GEps"        :: "[pttrn, bool] => 'a"               ("(3_./ _)" 10)
    1.20 -  "GAll"        :: "[idts, bool] => bool"             ("(3_./ _)" 10)
    1.21 -  "GEx"         :: "[idts, bool] => bool"             ("(3_./ _)" 10)
    1.22 -  "GEx1"        :: "[idts, bool] => bool"             ("(3!_./ _)" 10)
    1.23 -  ""           :: "[bool, bool] => bool"             (infixr 35)
    1.24 -  ""           :: "[bool, bool] => bool"             (infixr 30)
    1.25 -  ""          :: "[bool, bool] => bool"             (infixr 25)
    1.26 -
    1.27 -translations
    1.28 -(type)  "x  y"	== (type) "x => y" 
    1.29 -
    1.30 -(*  "x.t"	=> "%x.t" *)
    1.31 -
    1.32 -  "x  y"	== "x ~= y"
    1.33 -  " y"		== "~y"
    1.34 -  "x.P"	== "@x.P"
    1.35 -  "x.P"	== "! x. P"
    1.36 -  "x.P"	== "? x. P"
    1.37 -  "!x.P"	== "?! x. P"
    1.38 -  "x  y"	== "x & y"
    1.39 -  "x  y"	== "x | y"
    1.40 -  "x  y"	== "x --> y"
    1.41  (* end 8bit 1 *)
    1.42  
    1.43  end
    1.44 @@ -201,36 +167,6 @@
    1.45    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    1.46  
    1.47  (* start 8bit 2 *)
    1.48 -local open Ast;
    1.49 -fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
    1.50 -      fold_ast_p "" (unfold_ast "_asms" asms, concl)
    1.51 -  | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
    1.52 -fun impl_ast_tr' (*""*) asts =
    1.53 -  (case unfold_ast_p "" (Appl (Constant "" :: asts)) of
    1.54 -    (asms as _ :: _ :: _, concl)
    1.55 -      => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
    1.56 -  | _ => raise Match);
    1.57 -
    1.58 -in
    1.59 -val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr)::
    1.60 -				("Glam",    fn asts => Appl (Constant "_abs" :: asts))::
    1.61 -				parse_ast_translation;
    1.62 -
    1.63 -val print_ast_translation = ("", impl_ast_tr')::
    1.64 -				("_lambda", fn asts => Appl (Constant "Glam" :: asts)) ::	
    1.65 -				print_ast_translation;
    1.66 -
    1.67 -end;
    1.68 -
    1.69 -local open Syntax in
    1.70 -val thy = thy 
    1.71 -|> add_trrules_i 
    1.72 -[mk_appl (Constant "" ) [Variable "P", Variable "Q"] <-> 
    1.73 - mk_appl (Constant "==") [Variable "P", Variable "Q"],
    1.74 - mk_appl (Constant "" ) [Variable "P", Variable "Q"] <-> 
    1.75 - mk_appl (Constant "==>") [Variable "P", Variable "Q"],
    1.76 - (Constant "" ) <->  (Constant "!!")]
    1.77 -end;
    1.78  (* end 8bit 2 *)
    1.79  
    1.80