*** empty log message ***
authoroheimb
Tue Apr 23 17:01:51 1996 +0200 (1996-04-23)
changeset 167433aff4d854e4
parent 1673 d22110ddd0af
child 1675 36ba4da350c3
*** empty log message ***
index.html
src/HOL/HOL.thy
src/HOL/Nat.thy
src/HOL/Prod.thy
src/HOL/Set.thy
src/HOLCF/domain/theorems.ML
     1.1 --- a/index.html	Tue Apr 23 16:58:57 1996 +0200
     1.2 +++ b/index.html	Tue Apr 23 17:01:51 1996 +0200
     1.3 @@ -1,6 +1,8 @@
     1.4  <HTML><HEAD><TITLE>Isabelle Logics</TITLE></HEAD>
     1.5  <H2>Isabelle Logics</H2>
     1.6  Click on the logic's name to view a list of its theories.
     1.7 +
     1.8 +<!--
     1.9  <HR>
    1.10  First-Order Logic
    1.11  <UL>
    1.12 @@ -9,12 +11,17 @@
    1.13  <LI><A HREF = "CCL/index.html">CCL</A>
    1.14  <LI><A HREF = "LCF/index.html">LCF</A>
    1.15  </UL>
    1.16 +-->
    1.17 +
    1.18  <HR>
    1.19  Higher-Order Logic
    1.20  <UL>
    1.21  <LI><A HREF = "HOL/index.html">HOL</A>
    1.22  <LI><A HREF = "HOLCF/index.html">HOLCF</A>
    1.23 +<LI><A HREF = "FOCUS/index.html">FOCUS</A>
    1.24  </UL>
    1.25 +
    1.26 +<!--
    1.27  <HR>
    1.28  Sequent Calculus
    1.29  <UL>
    1.30 @@ -28,5 +35,8 @@
    1.31  <LI><A HREF = "Cube/index.html">Cube</A>
    1.32  <LI><A HREF = "FOLP/index.html">FOLP</A>
    1.33  </UL>
    1.34 +-->
    1.35 +
    1.36  <HR>
    1.37  </BODY></HTML>
    1.38 +
     2.1 --- a/src/HOL/HOL.thy	Tue Apr 23 16:58:57 1996 +0200
     2.2 +++ b/src/HOL/HOL.thy	Tue Apr 23 17:01:51 1996 +0200
     2.3 @@ -143,40 +143,6 @@
     2.4    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
     2.5  
     2.6  (* start 8bit 1 *)
     2.7 -types
     2.8 -('a, 'b) ""          (infixr 5)
     2.9 -
    2.10 -syntax
    2.11 -  ""		:: "['a::{}, 'a] => prop"       ("(_ / _)"         [3, 2] 2)
    2.12 -  ""		:: "[prop, prop] => prop"	("(_ / _)"        [2, 1] 1)
    2.13 -  "Gbigimpl"	:: "[asms, prop] => prop"	("((3 _ ) / _)" [0, 1] 1)
    2.14 -  "Gall"	:: "('a => prop) => prop"	(binder ""                0)
    2.15 -
    2.16 -  "Glam"         :: "[idts, 'a::logic] => 'b::logic"  ("(3_./ _)" 10)
    2.17 -  ""           :: "['a, 'a] => bool"                 (infixl 50)
    2.18 -  "Gnot"        :: "bool => bool"                     (" _" [40] 40)
    2.19 -  "GEps"        :: "[pttrn, bool] => 'a"               ("(3_./ _)" 10)
    2.20 -  "GAll"        :: "[idts, bool] => bool"             ("(3_./ _)" 10)
    2.21 -  "GEx"         :: "[idts, bool] => bool"             ("(3_./ _)" 10)
    2.22 -  "GEx1"        :: "[idts, bool] => bool"             ("(3!_./ _)" 10)
    2.23 -  ""           :: "[bool, bool] => bool"             (infixr 35)
    2.24 -  ""           :: "[bool, bool] => bool"             (infixr 30)
    2.25 -  ""          :: "[bool, bool] => bool"             (infixr 25)
    2.26 -
    2.27 -translations
    2.28 -(type)  "x  y"	== (type) "x => y" 
    2.29 -
    2.30 -(*  "x.t"	=> "%x.t" *)
    2.31 -
    2.32 -  "x  y"	== "x ~= y"
    2.33 -  " y"		== "~y"
    2.34 -  "x.P"	== "@x.P"
    2.35 -  "x.P"	== "! x. P"
    2.36 -  "x.P"	== "? x. P"
    2.37 -  "!x.P"	== "?! x. P"
    2.38 -  "x  y"	== "x & y"
    2.39 -  "x  y"	== "x | y"
    2.40 -  "x  y"	== "x --> y"
    2.41  (* end 8bit 1 *)
    2.42  
    2.43  end
    2.44 @@ -201,36 +167,6 @@
    2.45    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    2.46  
    2.47  (* start 8bit 2 *)
    2.48 -local open Ast;
    2.49 -fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
    2.50 -      fold_ast_p "" (unfold_ast "_asms" asms, concl)
    2.51 -  | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
    2.52 -fun impl_ast_tr' (*""*) asts =
    2.53 -  (case unfold_ast_p "" (Appl (Constant "" :: asts)) of
    2.54 -    (asms as _ :: _ :: _, concl)
    2.55 -      => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
    2.56 -  | _ => raise Match);
    2.57 -
    2.58 -in
    2.59 -val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr)::
    2.60 -				("Glam",    fn asts => Appl (Constant "_abs" :: asts))::
    2.61 -				parse_ast_translation;
    2.62 -
    2.63 -val print_ast_translation = ("", impl_ast_tr')::
    2.64 -				("_lambda", fn asts => Appl (Constant "Glam" :: asts)) ::	
    2.65 -				print_ast_translation;
    2.66 -
    2.67 -end;
    2.68 -
    2.69 -local open Syntax in
    2.70 -val thy = thy 
    2.71 -|> add_trrules_i 
    2.72 -[mk_appl (Constant "" ) [Variable "P", Variable "Q"] <-> 
    2.73 - mk_appl (Constant "==") [Variable "P", Variable "Q"],
    2.74 - mk_appl (Constant "" ) [Variable "P", Variable "Q"] <-> 
    2.75 - mk_appl (Constant "==>") [Variable "P", Variable "Q"],
    2.76 - (Constant "" ) <->  (Constant "!!")]
    2.77 -end;
    2.78  (* end 8bit 2 *)
    2.79  
    2.80  
     3.1 --- a/src/HOL/Nat.thy	Tue Apr 23 16:58:57 1996 +0200
     3.2 +++ b/src/HOL/Nat.thy	Tue Apr 23 17:01:51 1996 +0200
     3.3 @@ -77,11 +77,6 @@
     3.4    Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
     3.5  
     3.6  (* start 8bit 1 *)
     3.7 -syntax
     3.8 -  "Gmu"	:: (nat => bool) => nat				(binder "" 10)
     3.9 -
    3.10 -translations
    3.11 -  "x.P"	== "LEAST x. P"
    3.12  (* end 8bit 1 *)
    3.13  
    3.14  end
     4.1 --- a/src/HOL/Prod.thy	Tue Apr 23 16:58:57 1996 +0200
     4.2 +++ b/src/HOL/Prod.thy	Tue Apr 23 17:01:51 1996 +0200
     4.3 @@ -83,17 +83,6 @@
     4.4    Unity_def     "() == Abs_Unit(True)"
     4.5  
     4.6  (* start 8bit 1 *)
     4.7 -types
     4.8 -
     4.9 -('a, 'b) ""          (infixr 20)
    4.10 -
    4.11 -translations
    4.12 -
    4.13 -(type)  "x  y"	== (type) "x * y" 
    4.14 -
    4.15 -  "(x,y,zs).b"   == "split(x.(y,zs).b)"
    4.16 -  "(x,y).b"      == "split(x y.b)"
    4.17 -
    4.18  (* end 8bit 1 *)
    4.19  
    4.20  end
     5.1 --- a/src/HOL/Set.thy	Tue Apr 23 16:58:57 1996 +0200
     5.2 +++ b/src/HOL/Set.thy	Tue Apr 23 17:01:51 1996 +0200
     5.3 @@ -104,33 +104,6 @@
     5.4    surj_def      "surj(f)        == ! y. ? x. y=f(x)"
     5.5  
     5.6  (* start 8bit 1 *)
     5.7 -syntax
     5.8 -  ""		:: "['a set, 'a set] => 'a set"       (infixl 70)
     5.9 -  ""		:: "['a set, 'a set] => 'a set"       (infixl 65)
    5.10 -  ""		:: "['a, 'a set] => bool"             (infixl 50)
    5.11 -  ""		:: "['a, 'a set] => bool"             (infixl 50)
    5.12 -  GUnion	:: "(('a set)set) => 'a set"          ("_" [90] 90)
    5.13 -  GInter	:: "(('a set)set) => 'a set"          ("_" [90] 90)
    5.14 -  GUNION1       :: "['a => 'b set] => 'b set"         (binder " " 10)
    5.15 -  GINTER1       :: "['a => 'b set] => 'b set"         (binder " " 10)
    5.16 -  GINTER	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
    5.17 -  GUNION	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
    5.18 -  GBall		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
    5.19 -  GBex		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
    5.20 -
    5.21 -translations
    5.22 -  "x  y"      == "(x : y)"
    5.23 -  "x  y"      == "(x : y)"
    5.24 -  "x  y"      == "x Int y"
    5.25 -  "x  y"      == "x Un  y"
    5.26 -  "X"        == "Inter X" 
    5.27 -  "X"        == "Union X"
    5.28 -  "x.A"      == "INT x.A"
    5.29 -  "x.A"      == "UN x.A"
    5.30 -  "xA. B"   == "INT x:A. B"
    5.31 -  "xA. B"   == "UN x:A. B"
    5.32 -  "xA. P"    == "! x:A. P"
    5.33 -  "xA. P"    == "? x:A. P"
    5.34  (* end 8bit 1 *)
    5.35  
    5.36  end
     6.1 --- a/src/HOLCF/domain/theorems.ML	Tue Apr 23 16:58:57 1996 +0200
     6.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Apr 23 17:01:51 1996 +0200
     6.3 @@ -45,9 +45,9 @@
     6.4  in drep end;
     6.5  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
     6.6  
     6.7 -local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in
     6.8 +local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
     6.9  val kill_neq_tac = dtac trueI2 end;
    6.10 -fun case_UU_tac rews i v =	res_inst_tac [("Q",v^"=UU")] classical2 i THEN
    6.11 +fun case_UU_tac rews i v =	case_tac (v^"=UU") i THEN
    6.12  				asm_simp_tac (HOLCF_ss addsimps rews) i;
    6.13  
    6.14  val chain_tac = REPEAT_DETERM o resolve_tac