--- 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"
- "ÒxÎA. B" == "INT x:A. B"
- "ÓxÎA. B" == "UN x:A. B"
- "ÂxÎA. P" == "! x:A. P"
- "ÃxÎA. 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