Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
expanded tabs
authorclasohm
Mon, 05 Feb 1996 13:44:28 +0100
changeset 1473 e8d4606e6502
parent 1472 a89803e3d1bd
child 1474 3f7d67927fe2
expanded tabs
src/FOL/ex/List.thy file | annotate | diff | comparison | revisions
src/FOL/ex/Nat.thy file | annotate | diff | comparison | revisions
src/FOL/ex/Nat2.thy file | annotate | diff | comparison | revisions
src/FOL/ex/Prolog.thy file | annotate | diff | comparison | revisions
src/FOL/ex/foundn.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/ex/List.thy	Fri Feb 02 12:05:24 1996 +0100
+++ b/src/FOL/ex/List.thy	Mon Feb 05 13:44:28 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	FOL/ex/list
+(*  Title:      FOL/ex/list
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
 
 Examples of simplification and induction on lists
@@ -12,14 +12,14 @@
 arities list :: (term)term
 
 consts
-   hd		:: 'a list => 'a  
-   tl		:: 'a list => 'a list
-   forall	:: ['a list, 'a => o] => o  
-   len		:: 'a list => nat  
-   at		:: ['a list, nat] => 'a  
-   "[]"		:: ('a list)  	                     ("[]")
-   "."		:: ['a, 'a list] => 'a list          (infixr 80)
-   "++"		:: ['a list, 'a list] => 'a list     (infixr 70)
+   hd           :: 'a list => 'a  
+   tl           :: 'a list => 'a list
+   forall       :: ['a list, 'a => o] => o  
+   len          :: 'a list => nat  
+   at           :: ['a list, nat] => 'a  
+   "[]"         :: ('a list)                         ("[]")
+   "."          :: ['a, 'a list] => 'a list          (infixr 80)
+   "++"         :: ['a list, 'a list] => 'a list     (infixr 70)
 
 rules
  list_ind "[| P([]);  ALL x l. P(l)-->P(x.l) |] ==> All(P)"
@@ -30,12 +30,12 @@
  list_distinct1 "~[] = x.l"
  list_distinct2 "~x.l = []"
 
- list_free 	"x.l = x'.l' <-> x=x' & l=l'"
+ list_free      "x.l = x'.l' <-> x=x' & l=l'"
 
- app_nil 	"[]++l = l"
- app_cons 	"(x.l)++l' = x.(l++l')"
- tl_eq 	"tl(m.q) = q"
- hd_eq 	"hd(m.q) = m"
+ app_nil        "[]++l = l"
+ app_cons       "(x.l)++l' = x.(l++l')"
+ tl_eq  "tl(m.q) = q"
+ hd_eq  "hd(m.q) = m"
 
  forall_nil "forall([],P)"
  forall_cons "forall(x.l,P) <-> P(x) & forall(l,P)"
--- a/src/FOL/ex/Nat.thy	Fri Feb 02 12:05:24 1996 +0100
+++ b/src/FOL/ex/Nat.thy	Mon Feb 05 13:44:28 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	FOL/ex/nat.thy
+(*  Title:      FOL/ex/nat.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
 Examples for the manual "Introduction to Isabelle"
--- a/src/FOL/ex/Nat2.thy	Fri Feb 02 12:05:24 1996 +0100
+++ b/src/FOL/ex/Nat2.thy	Mon Feb 05 13:44:28 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	FOL/ex/nat2.thy
+(*  Title:      FOL/ex/nat2.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1994  University of Cambridge
 
 Theory for examples of simplification and induction on the natural numbers
@@ -13,28 +13,28 @@
 
 consts
  succ,pred :: nat => nat  
-       "0" :: nat  	("0")
+       "0" :: nat       ("0")
        "+" :: [nat,nat] => nat   (infixr 90)
   "<","<=" :: [nat,nat] => o     (infixr 70)
 
 rules
- pred_0		"pred(0) = 0"
- pred_succ	"pred(succ(m)) = m"
+ pred_0         "pred(0) = 0"
+ pred_succ      "pred(succ(m)) = m"
 
- plus_0		"0+n = n"
- plus_succ	"succ(m)+n = succ(m+n)"
+ plus_0         "0+n = n"
+ plus_succ      "succ(m)+n = succ(m+n)"
 
- nat_distinct1	"~ 0=succ(n)"
- nat_distinct2	"~ succ(m)=0"
- succ_inject	"succ(m)=succ(n) <-> m=n"
+ nat_distinct1  "~ 0=succ(n)"
+ nat_distinct2  "~ succ(m)=0"
+ succ_inject    "succ(m)=succ(n) <-> m=n"
 
- leq_0		"0 <= n"
- leq_succ_succ	"succ(m)<=succ(n) <-> m<=n"
- leq_succ_0	"~ succ(m) <= 0"
+ leq_0          "0 <= n"
+ leq_succ_succ  "succ(m)<=succ(n) <-> m<=n"
+ leq_succ_0     "~ succ(m) <= 0"
 
- lt_0_succ	"0 < succ(n)"
- lt_succ_succ	"succ(m)<succ(n) <-> m<n"
+ lt_0_succ      "0 < succ(n)"
+ lt_succ_succ   "succ(m)<succ(n) <-> m<n"
  lt_0 "~ m < 0"
 
- nat_ind	"[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
+ nat_ind        "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
 end
--- a/src/FOL/ex/Prolog.thy	Fri Feb 02 12:05:24 1996 +0100
+++ b/src/FOL/ex/Prolog.thy	Mon Feb 05 13:44:28 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	FOL/ex/prolog.thy
+(*  Title:      FOL/ex/prolog.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
 First-Order Logic: PROLOG examples
--- a/src/FOL/ex/foundn.ML	Fri Feb 02 12:05:24 1996 +0100
+++ b/src/FOL/ex/foundn.ML	Mon Feb 05 13:44:28 1996 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOL/ex/foundn
+(*  Title:      FOL/ex/foundn.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -6,7 +6,7 @@
 Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
 *)
 
-writeln"File FOL/ex/foundn.";
+writeln"File FOL/ex/foundn.ML";
 
 goal IFOL.thy "A&B  --> (C-->A&C)";
 by (rtac impI 1);
isabelle