*** empty log message ***
authoroheimb
Tue, 23 Apr 1996 17:01:51 +0200
changeset 1674 33aff4d854e4
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
--- a/index.html	Tue Apr 23 16:58:57 1996 +0200
+++ b/index.html	Tue Apr 23 17:01:51 1996 +0200
@@ -1,6 +1,8 @@
 <HTML><HEAD><TITLE>Isabelle Logics</TITLE></HEAD>
 <H2>Isabelle Logics</H2>
 Click on the logic's name to view a list of its theories.
+
+<!--
 <HR>
 First-Order Logic
 <UL>
@@ -9,12 +11,17 @@
 <LI><A HREF = "CCL/index.html">CCL</A>
 <LI><A HREF = "LCF/index.html">LCF</A>
 </UL>
+-->
+
 <HR>
 Higher-Order Logic
 <UL>
 <LI><A HREF = "HOL/index.html">HOL</A>
 <LI><A HREF = "HOLCF/index.html">HOLCF</A>
+<LI><A HREF = "FOCUS/index.html">FOCUS</A>
 </UL>
+
+<!--
 <HR>
 Sequent Calculus
 <UL>
@@ -28,5 +35,8 @@
 <LI><A HREF = "Cube/index.html">Cube</A>
 <LI><A HREF = "FOLP/index.html">FOLP</A>
 </UL>
+-->
+
 <HR>
 </BODY></HTML>
+
--- 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 *)
 
 
--- a/src/HOL/Nat.thy	Tue Apr 23 16:58:57 1996 +0200
+++ b/src/HOL/Nat.thy	Tue Apr 23 17:01:51 1996 +0200
@@ -77,11 +77,6 @@
   Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
 
 (* start 8bit 1 *)
-syntax
-  "Gmu"	:: (nat => bool) => nat				(binder "" 10)
-
-translations
-  "x.P"	== "LEAST x. P"
 (* end 8bit 1 *)
 
 end
--- a/src/HOL/Prod.thy	Tue Apr 23 16:58:57 1996 +0200
+++ b/src/HOL/Prod.thy	Tue Apr 23 17:01:51 1996 +0200
@@ -83,17 +83,6 @@
   Unity_def     "() == Abs_Unit(True)"
 
 (* start 8bit 1 *)
-types
-
-('a, 'b) ""          (infixr 20)
-
-translations
-
-(type)  "x  y"	== (type) "x * y" 
-
-  "(x,y,zs).b"   == "split(x.(y,zs).b)"
-  "(x,y).b"      == "split(x y.b)"
-
 (* end 8bit 1 *)
 
 end
--- a/src/HOL/Set.thy	Tue Apr 23 16:58:57 1996 +0200
+++ b/src/HOL/Set.thy	Tue Apr 23 17:01:51 1996 +0200
@@ -104,33 +104,6 @@
   surj_def      "surj(f)        == ! y. ? x. y=f(x)"
 
 (* start 8bit 1 *)
-syntax
-  ""		:: "['a set, 'a set] => 'a set"       (infixl 70)
-  ""		:: "['a set, 'a set] => 'a set"       (infixl 65)
-  ""		:: "['a, 'a set] => bool"             (infixl 50)
-  ""		:: "['a, 'a set] => bool"             (infixl 50)
-  GUnion	:: "(('a set)set) => 'a set"          ("_" [90] 90)
-  GInter	:: "(('a set)set) => 'a set"          ("_" [90] 90)
-  GUNION1       :: "['a => 'b set] => 'b set"         (binder " " 10)
-  GINTER1       :: "['a => 'b set] => 'b set"         (binder " " 10)
-  GINTER	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
-  GUNION	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
-  GBall		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
-  GBex		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
-
-translations
-  "x  y"      == "(x : y)"
-  "x  y"      == "(x : y)"
-  "x  y"      == "x Int y"
-  "x  y"      == "x Un  y"
-  "X"        == "Inter X" 
-  "X"        == "Union X"
-  "x.A"      == "INT x.A"
-  "x.A"      == "UN x.A"
-  "xA. B"   == "INT x:A. B"
-  "xA. B"   == "UN x:A. B"
-  "xA. P"    == "! x:A. P"
-  "xA. P"    == "? x:A. P"
 (* end 8bit 1 *)
 
 end
--- a/src/HOLCF/domain/theorems.ML	Tue Apr 23 16:58:57 1996 +0200
+++ b/src/HOLCF/domain/theorems.ML	Tue Apr 23 17:01:51 1996 +0200
@@ -45,9 +45,9 @@
 in drep end;
 val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
 
-local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in
+local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
 val kill_neq_tac = dtac trueI2 end;
-fun case_UU_tac rews i v =	res_inst_tac [("Q",v^"=UU")] classical2 i THEN
+fun case_UU_tac rews i v =	case_tac (v^"=UU") i THEN
 				asm_simp_tac (HOLCF_ss addsimps rews) i;
 
 val chain_tac = REPEAT_DETERM o resolve_tac